Proof Step: c_0_211

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

Proof State Overview

proof_step c_0_33 ⊕ times_times_real = ? c_0_176 ⊕ times_times_real X2244 X2245 = times_times_real X2245 X2244 c_0_33->c_0_176 c_0_211 ⊕ times_times_real X2 X4 = times_times_real X4 X2 c_0_176->c_0_211 c_0_240 ⊕ times_times_real X2 X4 = times_times_real X4 X2 c_0_211->c_0_240

Input Dependencies

c_0_33

Assumptions

c_0_176

Conclusion

c_0_211

Dependents

c_0_240

Formula

! [X4: real,X2: real] :
  ( ( times_times_real @ X2 @ X4 )
  = ( times_times_real @ X4 @ X2 ) )

Source

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