Proof Step: c_0_145

name: c_0_145 syntax: thf role: plain inference: fof_simplification

Proof State Overview

proof_step c_0_33 ⊕ times_times_real = ? c_0_145 ⊕ times_times_real X2092 X2093 = times_times_real X2093 X2092 c_0_33->c_0_145 c_0_176 ⊕ times_times_real X2244 X2245 = times_times_real X2245 X2244 c_0_145->c_0_176

Input Dependencies

c_0_33

Assumptions

c_0_33

Conclusion

c_0_145

Dependents

c_0_176

Formula

! [X2092: real,X2093: real] :
  ( ( times_times_real @ X2092 @ X2093 )
  = ( times_times_real @ X2093 @ X2092 ) )

Source

inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[c_0_33])])