`∀[a,b:ℝ].  ((a + b) = (b + a) ∈ ℝ)`

Proof

Definitions occuring in Statement :  radd: `a + b` real: `ℝ` uall: `∀[x:A]. B[x]` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` true: `True` uimplies: `b supposing a` all: `∀x:A. B[x]` squash: `↓T` prop: `ℙ` subtype_rel: `A ⊆r B` guard: `{T}` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` implies: `P `` Q`
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut hypothesis because_Cache sqequalRule sqequalHypSubstitution isect_memberEquality isectElimination thin hypothesisEquality axiomEquality natural_numberEquality extract_by_obid independent_isectElimination dependent_functionElimination applyEquality lambdaEquality imageElimination equalityTransitivity equalitySymmetry universeEquality imageMemberEquality baseClosed productElimination independent_functionElimination

Latex:
\mforall{}[a,b:\mBbbR{}].    ((a  +  b)  =  (b  +  a))

Date html generated: 2017_10_02-PM-07_15_26
Last ObjectModification: 2017_07_28-AM-07_20_29

Theory : reals

Home Index