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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  ceqsralt  3464  raltpd  4718  opiota  7908  mapsnend  8835  adderpqlem  10719  mulerpqlem  10720  lesub2  11479  rec11  11682  fimaxre  11928  fiminre  11931  avglt1  12220  ixxun  13104  modmuladdnn0  13644  hashdom  14103  hashle00  14124  hashf1lem1  14177  hashf1lem1OLD  14178  swrdspsleq  14387  repsdf2  14500  2shfti  14800  mulre  14841  rlim  15213  rlim2  15214  modremain  16126  nn0seqcvgd  16284  divgcdcoprm0  16379  prmreclem6  16631  pwsleval  17213  issubc  17559  ismgmid  18358  grpsubeq0  18670  grpsubadd  18672  gastacos  18925  orbsta  18928  lsslss  20232  prmirredlem  20703  zndvds  20766  zntoslem  20773  cygznlem1  20783  islindf2  21030  ismhp3  21342  coe1mul2lem1  21447  restcld  22332  leordtvallem1  22370  leordtvallem2  22371  ist1-2  22507  xkoccn  22779  qtopcld  22873  ordthmeolem  22961  qustgpopn  23280  isxmet2d  23489  prdsxmetlem  23530  xblss2  23564  imasf1oxms  23654  neibl  23666  xrtgioo  23978  xrsxmet  23981  isncvsngp  24322  minveclem4  24605  minveclem6  24607  minveclem7  24608  mbfmulc2lem  24820  mbfmax  24822  mbfi1fseqlem4  24892  itg2gt0  24934  itg2cnlem2  24936  iblpos  24966  logbgt0b  25952  angrteqvd  25965  affineequiv  25982  affineequiv2  25983  dcubic  26005  rlimcnp  26124  rlimcnp2  26125  efexple  26438  bposlem7  26447  lgsabs1  26493  lgsquadlem1  26537  m1lgs  26545  lnhl  26985  colinearalg  27287  axcontlem2  27342  nbupgrel  27721  nb3grpr  27758  usgr0edg0rusgr  27951  isspthonpth  28126  rusgrnumwwlkl1  28342  eupth2lem3lem4  28604  minvecolem4  29251  minvecolem6  29253  minvecolem7  29254  hvmulcan2  29444  xppreima  30992  eqg0el  31566  ply1chr  31678  smatrcl  31755  pstmxmet  31856  xrge0iifcnv  31892  ballotlemsima  32491  poimirlem27  35813  itg2addnclem  35837  itg2addnclem2  35838  iblabsnclem  35849  areacirclem2  35875  areacirclem4  35877  cvlcvrp  37361  ontric3g  41136  alephiso2  41172  sqrtcvallem1  41246  ntrclsk2  41685  ntrclsk13  41688  ntrneixb  41712  neicvgel1  41736  radcnvrat  41939  limsupmnflem  43268  logbge0b  45920  affinecomb2  46060  line2x  46111  itscnhlc0yqe  46116