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

Theorem 3bitr2d 308
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 283 . 2 (𝜑 → (𝜓𝜃))
4 3bitr2d.3 . 2 (𝜑 → (𝜃𝜏))
53, 4bitrd 280 1 (𝜑 → (𝜓𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207
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 208
This theorem is referenced by:  ceqsralt  3526  raltpd  4708  opiota  7746  mapsnend  8576  adderpqlem  10364  mulerpqlem  10365  lesub2  11123  rec11  11326  fimaxre  11572  fiminre  11576  avglt1  11863  ixxun  12742  modmuladdnn0  13271  hashdom  13728  hashle00  13749  hashf1lem1  13801  swrdspsleq  14015  repsdf2  14128  2shfti  14427  mulre  14468  rlim  14840  rlim2  14841  modremain  15747  nn0seqcvgd  15902  divgcdcoprm0  15997  prmreclem6  16245  pwsleval  16754  issubc  17093  ismgmid  17863  grpsubeq0  18123  grpsubadd  18125  gastacos  18378  orbsta  18381  lsslss  19662  coe1mul2lem1  20363  prmirredlem  20568  zndvds  20624  zntoslem  20631  cygznlem1  20641  islindf2  20886  restcld  21708  leordtvallem1  21746  leordtvallem2  21747  ist1-2  21883  xkoccn  22155  qtopcld  22249  ordthmeolem  22337  qustgpopn  22655  isxmet2d  22864  prdsxmetlem  22905  xblss2  22939  imasf1oxms  23026  neibl  23038  xrtgioo  23341  xrsxmet  23344  isncvsngp  23680  minveclem4  23962  minveclem6  23964  minveclem7  23965  mbfmulc2lem  24175  mbfmax  24177  mbfi1fseqlem4  24246  itg2gt0  24288  itg2cnlem2  24290  iblpos  24320  logbgt0b  25298  angrteqvd  25311  affineequiv  25328  affineequiv2  25329  dcubic  25351  rlimcnp  25470  rlimcnp2  25471  efexple  25784  bposlem7  25793  lgsabs1  25839  lgsquadlem1  25883  m1lgs  25891  lnhl  26328  colinearalg  26623  axcontlem2  26678  nbupgrel  27054  nb3grpr  27091  usgr0edg0rusgr  27284  isspthonpth  27457  rusgrnumwwlkl1  27674  eupth2lem3lem4  27937  minvecolem4  28584  minvecolem6  28586  minvecolem7  28587  hvmulcan2  28777  xppreima  30322  eqg0el  30853  smatrcl  30960  pstmxmet  31036  xrge0iifcnv  31075  ballotlemsima  31672  poimirlem27  34800  itg2addnclem  34824  itg2addnclem2  34825  iblabsnclem  34836  areacirclem2  34864  areacirclem4  34866  cvlcvrp  36356  ontric3g  39766  alephiso2  39795  ntrclsk2  40296  ntrclsk13  40299  ntrneixb  40323  neicvgel1  40347  radcnvrat  40523  limsupmnflem  41877  logbge0b  44551  affinecomb2  44618  line2x  44669  itscnhlc0yqe  44674
  Copyright terms: Public domain W3C validator