Nuprl Lemma : eu-cong-angle-symm2

`∀e:EuclideanPlane. ∀a,b,c,x,y,z:Point.  (xyz = abc `` abc = xyz)`

Proof

Definitions occuring in Statement :  eu-cong-angle: `abc = xyz` euclidean-plane: `EuclideanPlane` eu-point: `Point` all: `∀x:A. B[x]` implies: `P `` Q`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` euclidean-plane: `EuclideanPlane` eu-cong-angle: `abc = xyz` and: `P ∧ Q` exists: `∃x:A. B[x]` so_lambda: `λ2x.t[x]` so_apply: `x[s]` cand: `A c∧ B` uiff: `uiff(P;Q)` uimplies: `b supposing a`
Lemmas referenced :  eu-congruent-iff-length exists_wf eu-congruent_wf eu-between-eq_wf euclidean-plane_wf eu-point_wf eu-cong-angle_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis setElimination rename productElimination independent_pairFormation dependent_pairFormation productEquality because_Cache sqequalRule lambdaEquality dependent_functionElimination independent_isectElimination equalitySymmetry

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,x,y,z:Point.    (xyz  =  abc  {}\mRightarrow{}  abc  =  xyz)

Date html generated: 2016_06_16-PM-01_32_20
Last ObjectModification: 2016_05_23-PM-01_01_47

Theory : euclidean!geometry

Home Index