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  3224  raltpd  4306  opiota  7214  adderpqlem  9761  mulerpqlem  9762  lesub2  10508  rec11  10708  avglt1  11255  ixxun  12176  modmuladdnn0  12697  hashdom  13151  hashle00  13171  hashf1lem1  13222  swrdspsleq  13431  repsdf2  13506  2shfti  13801  mulre  13842  rlim  14207  rlim2  14208  modremain  15113  nn0seqcvgd  15264  divgcdcoprm0  15360  prmreclem6  15606  pwsleval  16134  issubc  16476  ismgmid  17245  grpsubeq0  17482  grpsubadd  17484  gastacos  17724  orbsta  17727  lsslss  18942  coe1mul2lem1  19618  prmirredlem  19822  zndvds  19879  zntoslem  19886  cygznlem1  19896  islindf2  20134  restcld  20957  leordtvallem1  20995  leordtvallem2  20996  ist1-2  21132  xkoccn  21403  qtopcld  21497  ordthmeolem  21585  qustgpopn  21904  isxmet2d  22113  prdsxmetlem  22154  xblss2  22188  imasf1oxms  22275  neibl  22287  xrtgioo  22590  xrsxmet  22593  isncvsngp  22930  minveclem4  23184  minveclem6  23186  minveclem7  23187  mbfmulc2lem  23395  mbfmax  23397  mbfi1fseqlem4  23466  itg2gt0  23508  itg2cnlem2  23510  iblpos  23540  angrteqvd  24517  affineequiv  24534  affineequiv2  24535  dcubic  24554  rlimcnp  24673  rlimcnp2  24674  efexple  24987  bposlem7  24996  lgsabs1  25042  lgsquadlem1  25086  m1lgs  25094  lnhl  25491  colinearalg  25771  axcontlem2  25826  nbupgrel  26222  nb3grpr  26265  usgr0edg0rusgr  26452  isspthonpth  26626  rusgrnumwwlkl1  26844  eupth2lem3lem4  27071  numclwlk1lem2f1  27198  minvecolem4  27706  minvecolem6  27708  minvecolem7  27709  hvmulcan2  27900  xppreima  29422  smatrcl  29836  pstmxmet  29914  xrge0iifcnv  29953  ballotlemsima  30551  poimirlem27  33407  itg2addnclem  33432  itg2addnclem2  33433  iblabsnclem  33444  areacirclem2  33472  areacirclem4  33474  cvlcvrp  34446  ntrclsk2  38186  ntrclsk13  38189  ntrneixb  38213  neicvgel1  38237  radcnvrat  38333  mapsnend  39207  limsupmnflem  39752  logbge0b  42122
  Copyright terms: Public domain W3C validator