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

Theorem 3bitr2d 294
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 269 . 2 (𝜑 → (𝜓𝜃))
4 3bitr2d.3 . 2 (𝜑 → (𝜃𝜏))
53, 4bitrd 266 1 (𝜑 → (𝜓𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
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 195
This theorem is referenced by:  ceqsralt  3198  raltpd  4254  opiota  7092  adderpqlem  9629  mulerpqlem  9630  lesub2  10369  rec11  10569  avglt1  11114  ixxun  12015  modmuladdnn0  12528  hashdom  12978  hashf1lem1  13045  swrdspsleq  13244  repsdf2  13319  2shfti  13611  mulre  13652  rlim  14017  rlim2  14018  modremain  14913  nn0seqcvgd  15064  divgcdcoprm0  15160  prmreclem6  15406  pwsleval  15919  issubc  16261  ismgmid  17030  grpsubeq0  17267  grpsubadd  17269  gastacos  17509  orbsta  17512  lsslss  18725  coe1mul2lem1  19401  prmirredlem  19602  zndvds  19659  zntoslem  19666  cygznlem1  19676  islindf2  19911  restcld  20725  leordtvallem1  20763  leordtvallem2  20764  ist1-2  20900  xkoccn  21171  qtopcld  21265  ordthmeolem  21353  qustgpopn  21672  isxmet2d  21880  prdsxmetlem  21921  xblss2  21955  imasf1oxms  22042  neibl  22054  xrtgioo  22346  xrsxmet  22349  isncvsngp  22680  minveclem4  22925  minveclem6  22927  minveclem7  22928  mbfmulc2lem  23134  mbfmax  23136  mbfi1fseqlem4  23205  itg2gt0  23247  itg2cnlem2  23249  iblpos  23279  angrteqvd  24250  affineequiv  24267  affineequiv2  24268  dcubic  24287  rlimcnp  24406  rlimcnp2  24407  efexple  24720  bposlem7  24729  lgsabs1  24775  lgsquadlem1  24819  m1lgs  24827  lnhl  25225  colinearalg  25505  axcontlem2  25560  nb3grapr  25745  el2wlksotot  26172  rusgranumwlkl1  26237  numclwlk1lem2f1  26384  minvecolem4  26923  minvecolem6  26925  minvecolem7  26926  hvmulcan2  27117  xppreima  28632  smatrcl  28993  pstmxmet  29071  xrge0iifcnv  29110  ballotlemsima  29707  poimirlem27  32406  itg2addnclem  32431  itg2addnclem2  32432  iblabsnclem  32443  areacirclem2  32471  areacirclem4  32473  cvlcvrp  33445  ntrclsk2  37186  ntrclsk13  37189  ntrneixb  37213  neicvgel1  37237  radcnvrat  37335  mapsnend  38186  nbupgrel  40566  nb3grpr  40609  usgr0edg0rusgr  40774  isspthonpth-av  40954  rusgrnumwwlkl1  41171  eupth2lem3lem4  41398  av-numclwlk1lem2f1  41523  logbge0b  42154
  Copyright terms: Public domain W3C validator