Quantum Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  QLE Home  >  Th. List  >  le3tr2 GIF version

Theorem le3tr2 141
 Description: Transitive inference useful for eliminating definitions.
Hypotheses
Ref Expression
le3tr2.1 ab
le3tr2.2 a = c
le3tr2.3 b = d
Assertion
Ref Expression
le3tr2 cd

Proof of Theorem le3tr2
StepHypRef Expression
1 le3tr2.1 . 2 ab
2 le3tr2.2 . . 3 a = c
32ax-r1 35 . 2 c = a
4 le3tr2.3 . . 3 b = d
54ax-r1 35 . 2 d = b
61, 3, 5le3tr1 140 1 cd
 Colors of variables: term Syntax hints:   = wb 1   ≤ wle 2 This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38 This theorem depends on definitions:  df-a 40  df-le1 130  df-le2 131 This theorem is referenced by:  ka4ot  435  3vded21  817  2oai1u  822  2oalem1  825  3vroa  831  mlaoml  833  sa5  836  neg3antlem2  865  elimconslem  867  elimcons  868  elimcons2  869  kb10iii  893  gomaex3lem6  919  oau  929  oa6v4v  933  oa4v3v  934  distoah2  941  distoah3  942  distoa  944  oa3to4lem6  950  oa6fromdualn  954  oa6to4  958  oa4to6  965  oa8to5  972  oa4to4u  973  oa3-2to2s  990  d3oa  995  mloa  1018  3oa2  1024  dp15lemc  1154  xdp15  1197  xxdp15  1200  xdp45lem  1202  xdp43lem  1203  xdp45  1204  xdp43  1205  3dp43  1206
 Copyright terms: Public domain W3C validator