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  4733  opiota  7997  mapsnend  8964  adderpqlem  10851  mulerpqlem  10852  lesub2  11618  rec11  11825  fimaxre  12072  fiminre  12075  avglt1  12365  ixxun  13267  modmuladdnn0  13828  hashdom  14292  hashle00  14313  hashf1lem1  14368  swrdspsleq  14579  repsdf2  14691  2shfti  14993  mulre  15034  rlim  15408  rlim2  15409  modremain  16325  nn0seqcvgd  16487  divgcdcoprm0  16582  prmreclem6  16839  pwsleval  17403  issubc  17748  ismgmid  18579  grpsubeq0  18945  grpsubadd  18947  eqg0el  19101  gastacos  19228  orbsta  19231  lsslss  20900  prmirredlem  21415  zndvds  21492  zntoslem  21499  cygznlem1  21509  islindf2  21757  ismhp3  22063  coe1mul2lem1  22187  ply1chr  22227  restcld  23093  leordtvallem1  23131  leordtvallem2  23132  ist1-2  23268  xkoccn  23540  qtopcld  23634  ordthmeolem  23722  qustgpopn  24041  isxmet2d  24248  prdsxmetlem  24289  xblss2  24323  imasf1oxms  24410  neibl  24422  xrtgioo  24728  xrsxmet  24731  isncvsngp  25082  minveclem4  25365  minveclem6  25367  minveclem7  25368  mbfmulc2lem  25581  mbfmax  25583  mbfi1fseqlem4  25652  itg2gt0  25694  itg2cnlem2  25696  iblpos  25727  r1pid2  26100  logbgt0b  26736  angrteqvd  26749  affineequiv  26766  affineequiv2  26767  dcubic  26789  rlimcnp  26908  rlimcnp2  26909  efexple  27225  bposlem7  27234  lgsabs1  27280  lgsquadlem1  27324  m1lgs  27332  subadds  28016  lnhl  28599  colinearalg  28895  axcontlem2  28950  nbupgrel  29330  nb3grpr  29367  usgr0edg0rusgr  29561  isspthonpth  29734  rusgrnumwwlkl1  29956  eupth2lem3lem4  30218  minvecolem4  30867  minvecolem6  30869  minvecolem7  30870  hvmulcan2  31060  xppreima  32634  fzo0opth  32792  fracerl  33279  dvdsrspss  33359  ply1degltel  33562  r1pid2OLD  33576  psrbasfsupp  33579  smatrcl  33816  pstmxmet  33917  xrge0iifcnv  33953  ballotlemsima  34536  poimirlem27  37693  itg2addnclem  37717  itg2addnclem2  37718  iblabsnclem  37729  areacirclem2  37755  areacirclem4  37757  cvlcvrp  39445  ontric3g  43620  alephiso2  43656  sqrtcvallem1  43729  ntrclsk2  44166  ntrclsk13  44169  ntrneixb  44193  neicvgel1  44217  radcnvrat  44412  limsupmnflem  45823  chnsubseqwl  46982  dfvopnbgr2  47958  pgnbgreunbgrlem2lem1  48219  pgnbgreunbgrlem2lem2  48220  logbge0b  48669  affinecomb2  48809  line2x  48860  itscnhlc0yqe  48865