Theorem 3bitr2d 307

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  raltpd  4725  opiota  8012  mapsnend  8983  adderpqlem  10877  mulerpqlem  10878  lesub2  11645  rec11  11853  fimaxre  12100  fiminre  12103  avglt1  12415  ixxun  13314  modmuladdnn0  13877  hashdom  14341  hashle00  14362  hashf1lem1  14417  swrdspsleq  14628  repsdf2  14740  2shfti  15042  mulre  15083  rlim  15457  rlim2  15458  modremain  16377  nn0seqcvgd  16539  divgcdcoprm0  16634  prmreclem6  16892  pwsleval  17457  issubc  17802  ismgmid  18633  grpsubeq0  19002  grpsubadd  19004  eqg0el  19158  gastacos  19285  orbsta  19288  lsslss  20956  prmirredlem  21452  zndvds  21529  zntoslem  21536  cygznlem1  21546  islindf2  21794  ismhp3  22108  coe1mul2lem1  22232  ply1chr  22271  restcld  23137  leordtvallem1  23175  leordtvallem2  23176  ist1-2  23312  xkoccn  23584  qtopcld  23678  ordthmeolem  23766  qustgpopn  24085  isxmet2d  24292  prdsxmetlem  24333  xblss2  24367  imasf1oxms  24454  neibl  24466  xrtgioo  24772  xrsxmet  24775  isncvsngp  25116  minveclem4  25399  minveclem6  25401  minveclem7  25402  mbfmulc2lem  25614  mbfmax  25616  mbfi1fseqlem4  25685  itg2gt0  25727  itg2cnlem2  25729  iblpos  25760  r1pid2  26127  logbgt0b  26757  angrteqvd  26770  affineequiv  26787  affineequiv2  26788  dcubic  26810  rlimcnp  26929  rlimcnp2  26930  efexple  27244  bposlem7  27253  lgsabs1  27299  lgsquadlem1  27343  m1lgs  27351  subadds  28062  lnhl  28683  colinearalg  28979  axcontlem2  29034  nbupgrel  29414  nb3grpr  29451  usgr0edg0rusgr  29644  isspthonpth  29817  rusgrnumwwlkl1  30039  eupth2lem3lem4  30301  minvecolem4  30951  minvecolem6  30953  minvecolem7  30954  hvmulcan2  31144  xppreima  32718  fzo0opth  32876  fracerl  33367  dvdsrspss  33447  ply1degltel  33654  r1pid2OLD  33669  psrbasfsupp  33672  smatrcl  33940  pstmxmet  34041  xrge0iifcnv  34077  ballotlemsima  34660  poimirlem27  37968  itg2addnclem  37992  itg2addnclem2  37993  iblabsnclem  38004  areacirclem2  38030  areacirclem4  38032  cvlcvrp  39786  ontric3g  43949  alephiso2  43985  sqrtcvallem1  44058  ntrclsk2  44495  ntrclsk13  44498  ntrneixb  44522  neicvgel1  44546  radcnvrat  44741  limsupmnflem  46148  chnsubseqwl  47309  nprmmul1  47987  dfvopnbgr2  48329  pgnbgreunbgrlem2lem1  48590  pgnbgreunbgrlem2lem2  48591  logbge0b  49039  affinecomb2  49179  line2x  49230  itscnhlc0yqe  49235