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  4738  opiota  8070  mapsnend  9067  adderpqlem  11042  mulerpqlem  11043  lesub2  11814  rec11  12018  fimaxre  12264  fiminre  12267  avglt1  12587  ixxun  13495  modmuladdnn0  14061  hashdom  14526  hashle00  14547  hashf1lem1  14603  swrdspsleq  14819  repsdf2  14933  2shfti  15238  mulre  15293  rlim  15667  rlim2  15668  modremain  16583  nn0seqcvgd  16750  divgcdcoprm0  16845  prmreclem6  17104  pwsleval  17670  issubc  18015  ismgmid  18850  grpsubeq0  19241  grpsubadd  19243  eqg0el  19403  gastacos  19529  orbsta  19532  lsslss  21241  prmirredlem  21783  zndvds  21860  zntoslem  21867  cygznlem1  21877  islindf2  22125  ismhp3  22468  coe1mul2lem1  22591  ply1chr  22629  restcld  23495  leordtvallem1  23533  leordtvallem2  23534  ist1-2  23670  xkoccn  23943  qtopcld  24037  ordthmeolem  24125  qustgpopn  24444  isxmet2d  24651  prdsxmetlem  24692  xblss2  24726  imasf1oxms  24813  neibl  24825  xrtgioo  25131  xrsxmet  25134  isncvsngp  25475  minveclem4  25758  minveclem6  25760  minveclem7  25761  mbfmulc2lem  25973  mbfmax  25975  mbfi1fseqlem4  26044  itg2gt0  26086  itg2cnlem2  26088  iblpos  26118  r1pid2  26485  logbgt0b  27126  angrteqvd  27139  affineequiv  27156  affineequiv2  27157  dcubic  27179  rlimcnp  27298  rlimcnp2  27299  efexple  27613  bposlem7  27622  lgsabs1  27668  lgsquadlem1  27712  m1lgs  27720  subadds  28461  lnhl  29086  elplng  29263  colinearalg  29493  axcontlem2  29548  nbupgrel  29931  nb3grpr  29968  usgr0edg0rusgr  30161  isspthonpth  30340  rusgrnumwwlkl1  30565  eupth2lem3lem4  30837  minvecolem4  31487  minvecolem6  31489  minvecolem7  31490  hvmulcan2  31680  xppreima  33286  fzo0opth  33441  fracerl  33914  dvdsrspss  33988  ply1degltel  34172  psrbasfsupp  34189  smatrcl  34474  pstmxmet  34575  xrge0iifcnv  34611  ballotlemsima  35194  poimirlem27  38658  itg2addnclem  38682  itg2addnclem2  38683  iblabsnclem  38694  areacirclem2  38720  areacirclem4  38722  cvlcvrp  40490  ontric3g  44616  alephiso2  44652  sqrtcvallem1  44724  ntrclsk2  45161  ntrclsk13  45164  ntrneixb  45188  neicvgel1  45212  radcnvrat  45391  limsupmnflem  46823  chnsubseqwl  47982  nprmmul1  48702  dfvopnbgr2  49044  pgnbgreunbgrlem2lem1  49305  pgnbgreunbgrlem2lem2  49306  logbge0b  49768  affinecomb2  49908  line2x  49959  itscnhlc0yqe  49964