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  4740  opiota  8013  mapsnend  8985  adderpqlem  10877  mulerpqlem  10878  lesub2  11644  rec11  11851  fimaxre  12098  fiminre  12101  avglt1  12391  ixxun  13289  modmuladdnn0  13850  hashdom  14314  hashle00  14335  hashf1lem1  14390  swrdspsleq  14601  repsdf2  14713  2shfti  15015  mulre  15056  rlim  15430  rlim2  15431  modremain  16347  nn0seqcvgd  16509  divgcdcoprm0  16604  prmreclem6  16861  pwsleval  17426  issubc  17771  ismgmid  18602  grpsubeq0  18968  grpsubadd  18970  eqg0el  19124  gastacos  19251  orbsta  19254  lsslss  20924  prmirredlem  21439  zndvds  21516  zntoslem  21523  cygznlem1  21533  islindf2  21781  ismhp3  22097  coe1mul2lem1  22221  ply1chr  22262  restcld  23128  leordtvallem1  23166  leordtvallem2  23167  ist1-2  23303  xkoccn  23575  qtopcld  23669  ordthmeolem  23757  qustgpopn  24076  isxmet2d  24283  prdsxmetlem  24324  xblss2  24358  imasf1oxms  24445  neibl  24457  xrtgioo  24763  xrsxmet  24766  isncvsngp  25117  minveclem4  25400  minveclem6  25402  minveclem7  25403  mbfmulc2lem  25616  mbfmax  25618  mbfi1fseqlem4  25687  itg2gt0  25729  itg2cnlem2  25731  iblpos  25762  r1pid2  26135  logbgt0b  26771  angrteqvd  26784  affineequiv  26801  affineequiv2  26802  dcubic  26824  rlimcnp  26943  rlimcnp2  26944  efexple  27260  bposlem7  27269  lgsabs1  27315  lgsquadlem1  27359  m1lgs  27367  subadds  28078  lnhl  28699  colinearalg  28995  axcontlem2  29050  nbupgrel  29430  nb3grpr  29467  usgr0edg0rusgr  29661  isspthonpth  29834  rusgrnumwwlkl1  30056  eupth2lem3lem4  30318  minvecolem4  30967  minvecolem6  30969  minvecolem7  30970  hvmulcan2  31160  xppreima  32734  fzo0opth  32893  fracerl  33399  dvdsrspss  33479  ply1degltel  33686  r1pid2OLD  33701  psrbasfsupp  33704  smatrcl  33973  pstmxmet  34074  xrge0iifcnv  34110  ballotlemsima  34693  poimirlem27  37892  itg2addnclem  37916  itg2addnclem2  37917  iblabsnclem  37928  areacirclem2  37954  areacirclem4  37956  cvlcvrp  39710  ontric3g  43872  alephiso2  43908  sqrtcvallem1  43981  ntrclsk2  44418  ntrclsk13  44421  ntrneixb  44445  neicvgel1  44469  radcnvrat  44664  limsupmnflem  46072  chnsubseqwl  47231  dfvopnbgr2  48207  pgnbgreunbgrlem2lem1  48468  pgnbgreunbgrlem2lem2  48469  logbge0b  48917  affinecomb2  49057  line2x  49108  itscnhlc0yqe  49113