Theorem 3bitr2d 309

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  raltpd  4739  opiota  8036  mapsnend  9013  adderpqlem  10909  mulerpqlem  10910  lesub2  11679  rec11  11886  fimaxre  12133  fiminre  12136  avglt1  12456  ixxun  13362  modmuladdnn0  13925  hashdom  14389  hashle00  14410  hashf1lem1  14465  swrdspsleq  14676  repsdf2  14788  2shfti  15090  mulre  15131  rlim  15505  rlim2  15506  modremain  16425  nn0seqcvgd  16587  divgcdcoprm0  16682  prmreclem6  16940  pwsleval  17506  issubc  17851  ismgmid  18682  grpsubeq0  19051  grpsubadd  19053  eqg0el  19207  gastacos  19333  orbsta  19336  lsslss  21008  prmirredlem  21504  zndvds  21581  zntoslem  21588  cygznlem1  21598  islindf2  21846  ismhp3  22187  coe1mul2lem1  22310  ply1chr  22349  restcld  23212  leordtvallem1  23250  leordtvallem2  23251  ist1-2  23387  xkoccn  23659  qtopcld  23753  ordthmeolem  23841  qustgpopn  24160  isxmet2d  24367  prdsxmetlem  24408  xblss2  24442  imasf1oxms  24529  neibl  24541  xrtgioo  24847  xrsxmet  24850  isncvsngp  25191  minveclem4  25474  minveclem6  25476  minveclem7  25477  mbfmulc2lem  25689  mbfmax  25691  mbfi1fseqlem4  25760  itg2gt0  25802  itg2cnlem2  25804  iblpos  25835  r1pid2  26202  logbgt0b  26835  angrteqvd  26848  affineequiv  26865  affineequiv2  26866  dcubic  26888  rlimcnp  27007  rlimcnp2  27008  efexple  27322  bposlem7  27331  lgsabs1  27377  lgsquadlem1  27421  m1lgs  27429  subadds  28140  lnhl  28761  colinearalg  29057  axcontlem2  29112  nbupgrel  29492  nb3grpr  29529  usgr0edg0rusgr  29722  isspthonpth  29895  rusgrnumwwlkl1  30117  eupth2lem3lem4  30379  minvecolem4  31029  minvecolem6  31031  minvecolem7  31032  hvmulcan2  31222  xppreima  32797  fzo0opth  32955  fracerl  33454  dvdsrspss  33534  ply1degltel  33751  r1pid2OLD  33766  psrbasfsupp  33769  smatrcl  34054  pstmxmet  34155  xrge0iifcnv  34191  ballotlemsima  34774  poimirlem27  38110  itg2addnclem  38134  itg2addnclem2  38135  iblabsnclem  38146  areacirclem2  38172  areacirclem4  38174  cvlcvrp  39928  ontric3g  44062  alephiso2  44098  sqrtcvallem1  44171  ntrclsk2  44608  ntrclsk13  44611  ntrneixb  44635  neicvgel1  44659  radcnvrat  44854  limsupmnflem  46258  chnsubseqwl  47419  nprmmul1  48097  dfvopnbgr2  48439  pgnbgreunbgrlem2lem1  48700  pgnbgreunbgrlem2lem2  48701  logbge0b  49149  affinecomb2  49289  line2x  49340  itscnhlc0yqe  49345