Proof Step: c_0_132

name: c_0_132 syntax: thf role: plain inference: split_conjunct

Proof State Overview

proof_step c_0_28 ⊕ ring_1_of_int_real one_one_int = one_one_real c_0_132 ⊕ ring_1_of_int_real one_one_int = one_one_real c_0_28->c_0_132 c_0_161 ⊕ ring_1_of_int_real one_one_int = one_one_real c_0_132->c_0_161

Input Dependencies

c_0_28

Assumptions

c_0_28

Conclusion

c_0_132

Dependents

c_0_161

Formula

( ( ring_1_of_int_real @ one_one_int )
= one_one_real )

Source

inference(split_conjunct,[status(thm)],[c_0_28])