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  3453  raltpd  4714  opiota  7872  mapsnend  8780  adderpqlem  10641  mulerpqlem  10642  lesub2  11400  rec11  11603  fimaxre  11849  fiminre  11852  avglt1  12141  ixxun  13024  modmuladdnn0  13563  hashdom  14022  hashle00  14043  hashf1lem1  14096  hashf1lem1OLD  14097  swrdspsleq  14306  repsdf2  14419  2shfti  14719  mulre  14760  rlim  15132  rlim2  15133  modremain  16045  nn0seqcvgd  16203  divgcdcoprm0  16298  prmreclem6  16550  pwsleval  17121  issubc  17466  ismgmid  18264  grpsubeq0  18576  grpsubadd  18578  gastacos  18831  orbsta  18834  lsslss  20138  prmirredlem  20606  zndvds  20669  zntoslem  20676  cygznlem1  20686  islindf2  20931  ismhp3  21243  coe1mul2lem1  21348  restcld  22231  leordtvallem1  22269  leordtvallem2  22270  ist1-2  22406  xkoccn  22678  qtopcld  22772  ordthmeolem  22860  qustgpopn  23179  isxmet2d  23388  prdsxmetlem  23429  xblss2  23463  imasf1oxms  23551  neibl  23563  xrtgioo  23875  xrsxmet  23878  isncvsngp  24218  minveclem4  24501  minveclem6  24503  minveclem7  24504  mbfmulc2lem  24716  mbfmax  24718  mbfi1fseqlem4  24788  itg2gt0  24830  itg2cnlem2  24832  iblpos  24862  logbgt0b  25848  angrteqvd  25861  affineequiv  25878  affineequiv2  25879  dcubic  25901  rlimcnp  26020  rlimcnp2  26021  efexple  26334  bposlem7  26343  lgsabs1  26389  lgsquadlem1  26433  m1lgs  26441  lnhl  26880  colinearalg  27181  axcontlem2  27236  nbupgrel  27615  nb3grpr  27652  usgr0edg0rusgr  27845  isspthonpth  28018  rusgrnumwwlkl1  28234  eupth2lem3lem4  28496  minvecolem4  29143  minvecolem6  29145  minvecolem7  29146  hvmulcan2  29336  xppreima  30884  eqg0el  31459  ply1chr  31571  smatrcl  31648  pstmxmet  31749  xrge0iifcnv  31785  ballotlemsima  32382  poimirlem27  35731  itg2addnclem  35755  itg2addnclem2  35756  iblabsnclem  35767  areacirclem2  35793  areacirclem4  35795  cvlcvrp  37281  ontric3g  41027  alephiso2  41054  sqrtcvallem1  41128  ntrclsk2  41567  ntrclsk13  41570  ntrneixb  41594  neicvgel1  41618  radcnvrat  41821  limsupmnflem  43151  logbge0b  45797  affinecomb2  45937  line2x  45988  itscnhlc0yqe  45993