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

Theorem le3tr1 140
Description: Transitive inference useful for introducing definitions. (Contributed by NM, 27-Aug-1997.)
Hypotheses
Ref Expression
le3tr1.1 ab
le3tr1.2 c = a
le3tr1.3 d = b
Assertion
Ref Expression
le3tr1 cd

Proof of Theorem le3tr1
StepHypRef Expression
1 le3tr1.2 . . 3 c = a
2 le3tr1.1 . . 3 ab
31, 2bltr 138 . 2 cb
4 le3tr1.3 . . 3 d = b
54ax-r1 35 . 2 b = d
63, 5lbtr 139 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:  le3tr2  141  lecon1  155  lelor  166  lelan  167  ledir  175  ledior  177  ka4lemo  228  ska13  241  i5lei1  347  i5lei2  348  i5lei3  349  i5lei4  350  id5leid0  351  wdf-c2  384  i3bi  496  i3th5  547  i3orlem5  556  ud4lem1a  577  u1lemc6  706  comi1  709  i2bi  722  u3lem14mp  794  3vth1  804  1oa  820  1oai1  821  mlalem  832  sa5  836  sadm3  838  bi3  839  negantlem2  849  negantlem3  850  negantlem9  859  negantlem10  861  neg3antlem2  865  comanb  872  mhlemlem2  875  mh  879  mlaconjo  886  cancellem  891  gomaex4  900  gomaex3h1  902  gomaex3h2  903  gomaex3h3  904  gomaex3h4  905  gomaex3h5  906  gomaex3h6  907  gomaex3h7  908  gomaex3h8  909  gomaex3h9  910  gomaex3h10  911  gomaex3h11  912  gomaex3h12  913  oa23  936  oa4lem1  937  oa4lem2  938  distoah4  943  oa3to4lem5  949  oa6todual  952  oa6fromdual  953  oa8todual  971  oal2  999  oal1  1000  oa3moa3  1029  lem3.3.3lem1  1049  lem3.3.3lem2  1050  lem3.3.5  1055  lem3.4.3  1076
  Copyright terms: Public domain W3C validator