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  3529  raltpd  4710  opiota  7748  mapsnend  8577  adderpqlem  10365  mulerpqlem  10366  lesub2  11124  rec11  11327  fimaxre  11573  fiminre  11577  avglt1  11864  ixxun  12744  modmuladdnn0  13273  hashdom  13730  hashle00  13751  hashf1lem1  13803  swrdspsleq  14017  repsdf2  14130  2shfti  14429  mulre  14470  rlim  14842  rlim2  14843  modremain  15749  nn0seqcvgd  15904  divgcdcoprm0  15999  prmreclem6  16247  pwsleval  16756  issubc  17095  ismgmid  17865  grpsubeq0  18125  grpsubadd  18127  gastacos  18380  orbsta  18383  lsslss  19664  coe1mul2lem1  20365  prmirredlem  20570  zndvds  20626  zntoslem  20633  cygznlem1  20643  islindf2  20888  restcld  21710  leordtvallem1  21748  leordtvallem2  21749  ist1-2  21885  xkoccn  22157  qtopcld  22251  ordthmeolem  22339  qustgpopn  22657  isxmet2d  22866  prdsxmetlem  22907  xblss2  22941  imasf1oxms  23028  neibl  23040  xrtgioo  23343  xrsxmet  23346  isncvsngp  23682  minveclem4  23964  minveclem6  23966  minveclem7  23967  mbfmulc2lem  24177  mbfmax  24179  mbfi1fseqlem4  24248  itg2gt0  24290  itg2cnlem2  24292  iblpos  24322  logbgt0b  25298  angrteqvd  25311  affineequiv  25328  affineequiv2  25329  dcubic  25351  rlimcnp  25471  rlimcnp2  25472  efexple  25785  bposlem7  25794  lgsabs1  25840  lgsquadlem1  25884  m1lgs  25892  lnhl  26329  colinearalg  26624  axcontlem2  26679  nbupgrel  27055  nb3grpr  27092  usgr0edg0rusgr  27285  isspthonpth  27458  rusgrnumwwlkl1  27675  eupth2lem3lem4  27938  minvecolem4  28585  minvecolem6  28587  minvecolem7  28588  hvmulcan2  28778  xppreima  30323  eqg0el  30854  smatrcl  30961  pstmxmet  31037  xrge0iifcnv  31076  ballotlemsima  31673  poimirlem27  34801  itg2addnclem  34825  itg2addnclem2  34826  iblabsnclem  34837  areacirclem2  34865  areacirclem4  34867  cvlcvrp  36358  ontric3g  39768  alephiso2  39797  ntrclsk2  40298  ntrclsk13  40301  ntrneixb  40325  neicvgel1  40349  radcnvrat  40526  limsupmnflem  41881  logbge0b  44521  affinecomb2  44588  line2x  44639  itscnhlc0yqe  44644
  Copyright terms: Public domain W3C validator