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

Theorem 3bitr2d 296
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 271 . 2 (𝜑 → (𝜓𝜃))
4 3bitr2d.3 . 2 (𝜑 → (𝜃𝜏))
53, 4bitrd 268 1 (𝜑 → (𝜓𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  ceqsralt  3260  raltpd  4346  opiota  7273  adderpqlem  9814  mulerpqlem  9815  lesub2  10561  rec11  10761  avglt1  11308  ixxun  12229  modmuladdnn0  12754  hashdom  13206  hashle00  13226  hashf1lem1  13277  swrdspsleq  13495  repsdf2  13571  2shfti  13864  mulre  13905  rlim  14270  rlim2  14271  modremain  15179  nn0seqcvgd  15330  divgcdcoprm0  15426  prmreclem6  15672  pwsleval  16200  issubc  16542  ismgmid  17311  grpsubeq0  17548  grpsubadd  17550  gastacos  17789  orbsta  17792  lsslss  19009  coe1mul2lem1  19685  prmirredlem  19889  zndvds  19946  zntoslem  19953  cygznlem1  19963  islindf2  20201  restcld  21024  leordtvallem1  21062  leordtvallem2  21063  ist1-2  21199  xkoccn  21470  qtopcld  21564  ordthmeolem  21652  qustgpopn  21970  isxmet2d  22179  prdsxmetlem  22220  xblss2  22254  imasf1oxms  22341  neibl  22353  xrtgioo  22656  xrsxmet  22659  isncvsngp  22995  minveclem4  23249  minveclem6  23251  minveclem7  23252  mbfmulc2lem  23459  mbfmax  23461  mbfi1fseqlem4  23530  itg2gt0  23572  itg2cnlem2  23574  iblpos  23604  angrteqvd  24581  affineequiv  24598  affineequiv2  24599  dcubic  24618  rlimcnp  24737  rlimcnp2  24738  efexple  25051  bposlem7  25060  lgsabs1  25106  lgsquadlem1  25150  m1lgs  25158  lnhl  25555  colinearalg  25835  axcontlem2  25890  nbupgrel  26286  nb3grpr  26328  usgr0edg0rusgr  26527  isspthonpth  26701  rusgrnumwwlkl1  26935  eupth2lem3lem4  27209  minvecolem4  27864  minvecolem6  27866  minvecolem7  27867  hvmulcan2  28058  xppreima  29577  smatrcl  29990  pstmxmet  30068  xrge0iifcnv  30107  ballotlemsima  30705  poimirlem27  33566  itg2addnclem  33591  itg2addnclem2  33592  iblabsnclem  33603  areacirclem2  33631  areacirclem4  33633  cvlcvrp  34945  ntrclsk2  38683  ntrclsk13  38686  ntrneixb  38710  neicvgel1  38734  radcnvrat  38830  mapsnend  39705  limsupmnflem  40270  logbge0b  42682
  Copyright terms: Public domain W3C validator