Theorem 3bitr2d 310

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  raltpd  4742  opiota  8071  mapsnend  9065  adderpqlem  11040  mulerpqlem  11041  lesub2  11812  rec11  12016  fimaxre  12262  fiminre  12265  avglt1  12585  ixxun  13493  modmuladdnn0  14059  hashdom  14524  hashle00  14545  hashf1lem1  14601  swrdspsleq  14816  repsdf2  14930  2shfti  15234  mulre  15289  rlim  15663  rlim2  15664  modremain  16579  nn0seqcvgd  16746  divgcdcoprm0  16841  prmreclem6  17100  pwsleval  17666  issubc  18011  ismgmid  18846  grpsubeq0  19237  grpsubadd  19239  eqg0el  19399  gastacos  19525  orbsta  19528  lsslss  21237  prmirredlem  21779  zndvds  21856  zntoslem  21863  cygznlem1  21873  islindf2  22121  ismhp3  22464  coe1mul2lem1  22587  ply1chr  22625  restcld  23491  leordtvallem1  23529  leordtvallem2  23530  ist1-2  23666  xkoccn  23939  qtopcld  24033  ordthmeolem  24121  qustgpopn  24440  isxmet2d  24647  prdsxmetlem  24688  xblss2  24722  imasf1oxms  24809  neibl  24821  xrtgioo  25127  xrsxmet  25130  isncvsngp  25471  minveclem4  25754  minveclem6  25756  minveclem7  25757  mbfmulc2lem  25969  mbfmax  25971  mbfi1fseqlem4  26040  itg2gt0  26082  itg2cnlem2  26084  iblpos  26114  r1pid2  26481  logbgt0b  27122  angrteqvd  27135  affineequiv  27152  affineequiv2  27153  dcubic  27175  rlimcnp  27294  rlimcnp2  27295  efexple  27609  bposlem7  27618  lgsabs1  27664  lgsquadlem1  27708  m1lgs  27716  subadds  28457  lnhl  29082  elplng  29259  colinearalg  29489  axcontlem2  29544  nbupgrel  29927  nb3grpr  29964  usgr0edg0rusgr  30157  isspthonpth  30336  rusgrnumwwlkl1  30561  eupth2lem3lem4  30833  minvecolem4  31483  minvecolem6  31485  minvecolem7  31486  hvmulcan2  31676  xppreima  33240  fzo0opth  33396  fracerl  33869  dvdsrspss  33943  ply1degltel  34127  psrbasfsupp  34144  smatrcl  34429  pstmxmet  34530  xrge0iifcnv  34566  ballotlemsima  35149  poimirlem27  38567  itg2addnclem  38591  itg2addnclem2  38592  iblabsnclem  38603  areacirclem2  38629  areacirclem4  38631  cvlcvrp  40399  ontric3g  44524  alephiso2  44560  sqrtcvallem1  44632  ntrclsk2  45069  ntrclsk13  45072  ntrneixb  45096  neicvgel1  45120  radcnvrat  45299  limsupmnflem  46731  chnsubseqwl  47890  nprmmul1  48610  dfvopnbgr2  48952  pgnbgreunbgrlem2lem1  49213  pgnbgreunbgrlem2lem2  49214  logbge0b  49676  affinecomb2  49816  line2x  49867  itscnhlc0yqe  49872