Theorem 3bitr2d 306

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 281	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4		3bitr2d.3	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
5	3, 4	bitrd 278	1 ⊢ (𝜑 → (𝜓 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  ceqsralt  3472  raltpd  4729  opiota  7967  mapsnend  8901  adderpqlem  10811  mulerpqlem  10812  lesub2  11571  rec11  11774  fimaxre  12020  fiminre  12023  avglt1  12312  ixxun  13196  modmuladdnn0  13736  hashdom  14194  hashle00  14215  hashf1lem1  14268  hashf1lem1OLD  14269  swrdspsleq  14476  repsdf2  14589  2shfti  14890  mulre  14931  rlim  15303  rlim2  15304  modremain  16216  nn0seqcvgd  16372  divgcdcoprm0  16467  prmreclem6  16719  pwsleval  17301  issubc  17647  ismgmid  18446  grpsubeq0  18757  grpsubadd  18759  gastacos  19012  orbsta  19015  lsslss  20329  prmirredlem  20800  zndvds  20863  zntoslem  20870  cygznlem1  20880  islindf2  21127  ismhp3  21439  coe1mul2lem1  21544  restcld  22429  leordtvallem1  22467  leordtvallem2  22468  ist1-2  22604  xkoccn  22876  qtopcld  22970  ordthmeolem  23058  qustgpopn  23377  isxmet2d  23586  prdsxmetlem  23627  xblss2  23661  imasf1oxms  23751  neibl  23763  xrtgioo  24075  xrsxmet  24078  isncvsngp  24419  minveclem4  24702  minveclem6  24704  minveclem7  24705  mbfmulc2lem  24917  mbfmax  24919  mbfi1fseqlem4  24989  itg2gt0  25031  itg2cnlem2  25033  iblpos  25063  logbgt0b  26049  angrteqvd  26062  affineequiv  26079  affineequiv2  26080  dcubic  26102  rlimcnp  26221  rlimcnp2  26222  efexple  26535  bposlem7  26544  lgsabs1  26590  lgsquadlem1  26634  m1lgs  26642  lnhl  27265  colinearalg  27567  axcontlem2  27622  nbupgrel  28001  nb3grpr  28038  usgr0edg0rusgr  28231  isspthonpth  28405  rusgrnumwwlkl1  28621  eupth2lem3lem4  28883  minvecolem4  29530  minvecolem6  29532  minvecolem7  29533  hvmulcan2  29723  xppreima  31270  eqg0el  31853  ply1chr  31966  smatrcl  32044  pstmxmet  32145  xrge0iifcnv  32181  ballotlemsima  32782  poimirlem27  35909  itg2addnclem  35933  itg2addnclem2  35934  iblabsnclem  35945  areacirclem2  35971  areacirclem4  35973  cvlcvrp  37607  ontric3g  41451  alephiso2  41487  sqrtcvallem1  41560  ntrclsk2  41999  ntrclsk13  42002  ntrneixb  42026  neicvgel1  42050  radcnvrat  42253  limsupmnflem  43597  logbge0b  46260  affinecomb2  46400  line2x  46451  itscnhlc0yqe  46456