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

Theorem 3bitr2d 309
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 284 . 2 (𝜑 → (𝜓𝜃))
4 3bitr2d.3 . 2 (𝜑 → (𝜃𝜏))
53, 4bitrd 281 1 (𝜑 → (𝜓𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208
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 209
This theorem is referenced by:  ceqsralt  3507  raltpd  4692  opiota  7735  mapsnend  8566  adderpqlem  10354  mulerpqlem  10355  lesub2  11113  rec11  11316  fimaxre  11562  fiminre  11566  avglt1  11854  ixxun  12733  modmuladdnn0  13267  hashdom  13725  hashle00  13746  hashf1lem1  13798  swrdspsleq  14007  repsdf2  14120  2shfti  14419  mulre  14460  rlim  14832  rlim2  14833  modremain  15737  nn0seqcvgd  15892  divgcdcoprm0  15987  prmreclem6  16235  pwsleval  16745  issubc  17084  ismgmid  17854  grpsubeq0  18164  grpsubadd  18166  gastacos  18419  orbsta  18422  lsslss  19709  coe1mul2lem1  20411  prmirredlem  20616  zndvds  20672  zntoslem  20679  cygznlem1  20689  islindf2  20934  restcld  21756  leordtvallem1  21794  leordtvallem2  21795  ist1-2  21931  xkoccn  22203  qtopcld  22297  ordthmeolem  22385  qustgpopn  22704  isxmet2d  22913  prdsxmetlem  22954  xblss2  22988  imasf1oxms  23075  neibl  23087  xrtgioo  23390  xrsxmet  23393  isncvsngp  23733  minveclem4  24015  minveclem6  24017  minveclem7  24018  mbfmulc2lem  24230  mbfmax  24232  mbfi1fseqlem4  24301  itg2gt0  24343  itg2cnlem2  24345  iblpos  24375  logbgt0b  25358  angrteqvd  25371  affineequiv  25388  affineequiv2  25389  dcubic  25411  rlimcnp  25530  rlimcnp2  25531  efexple  25844  bposlem7  25853  lgsabs1  25899  lgsquadlem1  25943  m1lgs  25951  lnhl  26388  colinearalg  26683  axcontlem2  26738  nbupgrel  27114  nb3grpr  27151  usgr0edg0rusgr  27344  isspthonpth  27517  rusgrnumwwlkl1  27733  eupth2lem3lem4  27995  minvecolem4  28642  minvecolem6  28644  minvecolem7  28645  hvmulcan2  28835  xppreima  30381  eqg0el  30934  smatrcl  31072  pstmxmet  31148  xrge0iifcnv  31184  ballotlemsima  31781  poimirlem27  34960  itg2addnclem  34984  itg2addnclem2  34985  iblabsnclem  34996  areacirclem2  35022  areacirclem4  35024  cvlcvrp  36512  ontric3g  40023  alephiso2  40052  ntrclsk2  40553  ntrclsk13  40556  ntrneixb  40580  neicvgel1  40604  radcnvrat  40801  limsupmnflem  42153  logbge0b  44768  affinecomb2  44877  line2x  44928  itscnhlc0yqe  44933
  Copyright terms: Public domain W3C validator