Theorem 3bitr2d 309

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

Step	Hyp	Ref	Expression
1		3bitr2d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		3bitr2d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
3	1, 2	bitr4d 284	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4		3bitr2d.3	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
5	3, 4	bitrd 281	1 ⊢ (𝜑 → (𝜓 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  ceqsralt  3528  raltpd  4716  opiota  7757  mapsnend  8588  adderpqlem  10376  mulerpqlem  10377  lesub2  11135  rec11  11338  fimaxre  11584  fiminre  11588  avglt1  11876  ixxun  12755  modmuladdnn0  13284  hashdom  13741  hashle00  13762  hashf1lem1  13814  swrdspsleq  14027  repsdf2  14140  2shfti  14439  mulre  14480  rlim  14852  rlim2  14853  modremain  15759  nn0seqcvgd  15914  divgcdcoprm0  16009  prmreclem6  16257  pwsleval  16766  issubc  17105  ismgmid  17875  grpsubeq0  18185  grpsubadd  18187  gastacos  18440  orbsta  18443  lsslss  19733  coe1mul2lem1  20435  prmirredlem  20640  zndvds  20696  zntoslem  20703  cygznlem1  20713  islindf2  20958  restcld  21780  leordtvallem1  21818  leordtvallem2  21819  ist1-2  21955  xkoccn  22227  qtopcld  22321  ordthmeolem  22409  qustgpopn  22728  isxmet2d  22937  prdsxmetlem  22978  xblss2  23012  imasf1oxms  23099  neibl  23111  xrtgioo  23414  xrsxmet  23417  isncvsngp  23753  minveclem4  24035  minveclem6  24037  minveclem7  24038  mbfmulc2lem  24248  mbfmax  24250  mbfi1fseqlem4  24319  itg2gt0  24361  itg2cnlem2  24363  iblpos  24393  logbgt0b  25371  angrteqvd  25384  affineequiv  25401  affineequiv2  25402  dcubic  25424  rlimcnp  25543  rlimcnp2  25544  efexple  25857  bposlem7  25866  lgsabs1  25912  lgsquadlem1  25956  m1lgs  25964  lnhl  26401  colinearalg  26696  axcontlem2  26751  nbupgrel  27127  nb3grpr  27164  usgr0edg0rusgr  27357  isspthonpth  27530  rusgrnumwwlkl1  27747  eupth2lem3lem4  28010  minvecolem4  28657  minvecolem6  28659  minvecolem7  28660  hvmulcan2  28850  xppreima  30394  eqg0el  30926  smatrcl  31061  pstmxmet  31137  xrge0iifcnv  31176  ballotlemsima  31773  poimirlem27  34934  itg2addnclem  34958  itg2addnclem2  34959  iblabsnclem  34970  areacirclem2  34998  areacirclem4  35000  cvlcvrp  36491  ontric3g  39937  alephiso2  39966  ntrclsk2  40467  ntrclsk13  40470  ntrneixb  40494  neicvgel1  40518  radcnvrat  40695  limsupmnflem  42050  logbge0b  44672  affinecomb2  44739  line2x  44790  itscnhlc0yqe  44795