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:  raltpd  4784  opiota  8047  mapsnend  9038  adderpqlem  10951  mulerpqlem  10952  lesub2  11713  rec11  11916  fimaxre  12162  fiminre  12165  avglt1  12454  ixxun  13344  modmuladdnn0  13884  hashdom  14343  hashle00  14364  hashf1lem1  14419  hashf1lem1OLD  14420  swrdspsleq  14619  repsdf2  14732  2shfti  15031  mulre  15072  rlim  15443  rlim2  15444  modremain  16355  nn0seqcvgd  16511  divgcdcoprm0  16606  prmreclem6  16858  pwsleval  17443  issubc  17789  ismgmid  18590  grpsubeq0  18945  grpsubadd  18947  gastacos  19215  orbsta  19218  lsslss  20716  prmirredlem  21243  zndvds  21324  zntoslem  21331  cygznlem1  21341  islindf2  21588  ismhp3  21905  coe1mul2lem1  22009  restcld  22896  leordtvallem1  22934  leordtvallem2  22935  ist1-2  23071  xkoccn  23343  qtopcld  23437  ordthmeolem  23525  qustgpopn  23844  isxmet2d  24053  prdsxmetlem  24094  xblss2  24128  imasf1oxms  24218  neibl  24230  xrtgioo  24542  xrsxmet  24545  isncvsngp  24897  minveclem4  25180  minveclem6  25182  minveclem7  25183  mbfmulc2lem  25396  mbfmax  25398  mbfi1fseqlem4  25468  itg2gt0  25510  itg2cnlem2  25512  iblpos  25542  logbgt0b  26534  angrteqvd  26547  affineequiv  26564  affineequiv2  26565  dcubic  26587  rlimcnp  26706  rlimcnp2  26707  efexple  27020  bposlem7  27029  lgsabs1  27075  lgsquadlem1  27119  m1lgs  27127  subadds  27777  lnhl  28133  colinearalg  28435  axcontlem2  28490  nbupgrel  28869  nb3grpr  28906  usgr0edg0rusgr  29099  isspthonpth  29273  rusgrnumwwlkl1  29489  eupth2lem3lem4  29751  minvecolem4  30400  minvecolem6  30402  minvecolem7  30403  hvmulcan2  30593  xppreima  32138  eqg0el  32747  dvdsrspss  32765  ply1chr  32935  ply1degltel  32940  r1pid2  32954  smatrcl  33074  pstmxmet  33175  xrge0iifcnv  33211  ballotlemsima  33812  poimirlem27  36818  itg2addnclem  36842  itg2addnclem2  36843  iblabsnclem  36854  areacirclem2  36880  areacirclem4  36882  cvlcvrp  38513  ontric3g  42575  alephiso2  42611  sqrtcvallem1  42684  ntrclsk2  43121  ntrclsk13  43124  ntrneixb  43148  neicvgel1  43172  radcnvrat  43375  limsupmnflem  44734  logbge0b  47336  affinecomb2  47476  line2x  47527  itscnhlc0yqe  47532