MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3bitr2d Structured version   Visualization version   GIF version

Theorem 3bitr2d 307
Description: Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)
Hypotheses
Ref Expression
3bitr2d.1 (𝜑 → (𝜓𝜒))
3bitr2d.2 (𝜑 → (𝜃𝜒))
3bitr2d.3 (𝜑 → (𝜃𝜏))
Assertion
Ref Expression
3bitr2d (𝜑 → (𝜓𝜏))

Proof of Theorem 3bitr2d
StepHypRef Expression
1 3bitr2d.1 . . 3 (𝜑 → (𝜓𝜒))
2 3bitr2d.2 . . 3 (𝜑 → (𝜃𝜒))
31, 2bitr4d 282 . 2 (𝜑 → (𝜓𝜃))
4 3bitr2d.3 . 2 (𝜑 → (𝜃𝜏))
53, 4bitrd 279 1 (𝜑 → (𝜓𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 206
This theorem is referenced by:  ceqsralt  3477  raltpd  4743  opiota  7992  mapsnend  8981  adderpqlem  10891  mulerpqlem  10892  lesub2  11651  rec11  11854  fimaxre  12100  fiminre  12103  avglt1  12392  ixxun  13281  modmuladdnn0  13821  hashdom  14280  hashle00  14301  hashf1lem1  14354  hashf1lem1OLD  14355  swrdspsleq  14554  repsdf2  14667  2shfti  14966  mulre  15007  rlim  15378  rlim2  15379  modremain  16291  nn0seqcvgd  16447  divgcdcoprm0  16542  prmreclem6  16794  pwsleval  17376  issubc  17722  ismgmid  18521  grpsubeq0  18834  grpsubadd  18836  gastacos  19091  orbsta  19094  lsslss  20425  prmirredlem  20896  zndvds  20959  zntoslem  20966  cygznlem1  20976  islindf2  21223  ismhp3  21536  coe1mul2lem1  21641  restcld  22526  leordtvallem1  22564  leordtvallem2  22565  ist1-2  22701  xkoccn  22973  qtopcld  23067  ordthmeolem  23155  qustgpopn  23474  isxmet2d  23683  prdsxmetlem  23724  xblss2  23758  imasf1oxms  23848  neibl  23860  xrtgioo  24172  xrsxmet  24175  isncvsngp  24516  minveclem4  24799  minveclem6  24801  minveclem7  24802  mbfmulc2lem  25014  mbfmax  25016  mbfi1fseqlem4  25086  itg2gt0  25128  itg2cnlem2  25130  iblpos  25160  logbgt0b  26146  angrteqvd  26159  affineequiv  26176  affineequiv2  26177  dcubic  26199  rlimcnp  26318  rlimcnp2  26319  efexple  26632  bposlem7  26641  lgsabs1  26687  lgsquadlem1  26731  m1lgs  26739  subadds  27360  lnhl  27560  colinearalg  27862  axcontlem2  27917  nbupgrel  28296  nb3grpr  28333  usgr0edg0rusgr  28526  isspthonpth  28700  rusgrnumwwlkl1  28916  eupth2lem3lem4  29178  minvecolem4  29825  minvecolem6  29827  minvecolem7  29828  hvmulcan2  30018  xppreima  31565  eqg0el  32152  ply1chr  32285  smatrcl  32380  pstmxmet  32481  xrge0iifcnv  32517  ballotlemsima  33118  poimirlem27  36108  itg2addnclem  36132  itg2addnclem2  36133  iblabsnclem  36144  areacirclem2  36170  areacirclem4  36172  cvlcvrp  37805  ontric3g  41801  alephiso2  41837  sqrtcvallem1  41910  ntrclsk2  42347  ntrclsk13  42350  ntrneixb  42374  neicvgel1  42398  radcnvrat  42601  limsupmnflem  43968  logbge0b  46656  affinecomb2  46796  line2x  46847  itscnhlc0yqe  46852
  Copyright terms: Public domain W3C validator