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  4757  opiota  8058  mapsnend  9050  adderpqlem  10968  mulerpqlem  10969  lesub2  11732  rec11  11939  fimaxre  12186  fiminre  12189  avglt1  12479  ixxun  13378  modmuladdnn0  13933  hashdom  14397  hashle00  14418  hashf1lem1  14473  swrdspsleq  14683  repsdf2  14796  2shfti  15099  mulre  15140  rlim  15511  rlim2  15512  modremain  16427  nn0seqcvgd  16589  divgcdcoprm0  16684  prmreclem6  16941  pwsleval  17507  issubc  17848  ismgmid  18643  grpsubeq0  19009  grpsubadd  19011  eqg0el  19166  gastacos  19293  orbsta  19296  lsslss  20918  prmirredlem  21433  zndvds  21510  zntoslem  21517  cygznlem1  21527  islindf2  21774  ismhp3  22080  coe1mul2lem1  22204  ply1chr  22244  restcld  23110  leordtvallem1  23148  leordtvallem2  23149  ist1-2  23285  xkoccn  23557  qtopcld  23651  ordthmeolem  23739  qustgpopn  24058  isxmet2d  24266  prdsxmetlem  24307  xblss2  24341  imasf1oxms  24428  neibl  24440  xrtgioo  24746  xrsxmet  24749  isncvsngp  25101  minveclem4  25384  minveclem6  25386  minveclem7  25387  mbfmulc2lem  25600  mbfmax  25602  mbfi1fseqlem4  25671  itg2gt0  25713  itg2cnlem2  25715  iblpos  25746  r1pid2  26119  logbgt0b  26755  angrteqvd  26768  affineequiv  26785  affineequiv2  26786  dcubic  26808  rlimcnp  26927  rlimcnp2  26928  efexple  27244  bposlem7  27253  lgsabs1  27299  lgsquadlem1  27343  m1lgs  27351  subadds  28026  lnhl  28594  colinearalg  28889  axcontlem2  28944  nbupgrel  29324  nb3grpr  29361  usgr0edg0rusgr  29555  isspthonpth  29731  rusgrnumwwlkl1  29950  eupth2lem3lem4  30212  minvecolem4  30861  minvecolem6  30863  minvecolem7  30864  hvmulcan2  31054  xppreima  32623  fzo0opth  32782  fracerl  33300  dvdsrspss  33402  ply1degltel  33604  r1pid2OLD  33618  smatrcl  33827  pstmxmet  33928  xrge0iifcnv  33964  ballotlemsima  34548  poimirlem27  37671  itg2addnclem  37695  itg2addnclem2  37696  iblabsnclem  37707  areacirclem2  37733  areacirclem4  37735  cvlcvrp  39358  ontric3g  43546  alephiso2  43582  sqrtcvallem1  43655  ntrclsk2  44092  ntrclsk13  44095  ntrneixb  44119  neicvgel1  44143  radcnvrat  44338  limsupmnflem  45749  dfvopnbgr2  47866  logbge0b  48543  affinecomb2  48683  line2x  48734  itscnhlc0yqe  48739