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 ⊢ (𝜑 → (𝜓 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  ceqsralt  3475  raltpd  4677  opiota  7739  mapsnend  8571  adderpqlem  10365  mulerpqlem  10366  lesub2  11124  rec11  11327  fimaxre  11573  fiminre  11576  avglt1  11863  ixxun  12742  modmuladdnn0  13278  hashdom  13736  hashle00  13757  hashf1lem1  13809  swrdspsleq  14018  repsdf2  14131  2shfti  14431  mulre  14472  rlim  14844  rlim2  14845  modremain  15749  nn0seqcvgd  15904  divgcdcoprm0  15999  prmreclem6  16247  pwsleval  16758  issubc  17097  ismgmid  17867  grpsubeq0  18177  grpsubadd  18179  gastacos  18432  orbsta  18435  lsslss  19726  prmirredlem  20186  zndvds  20241  zntoslem  20248  cygznlem1  20258  islindf2  20503  coe1mul2lem1  20896  restcld  21777  leordtvallem1  21815  leordtvallem2  21816  ist1-2  21952  xkoccn  22224  qtopcld  22318  ordthmeolem  22406  qustgpopn  22725  isxmet2d  22934  prdsxmetlem  22975  xblss2  23009  imasf1oxms  23096  neibl  23108  xrtgioo  23411  xrsxmet  23414  isncvsngp  23754  minveclem4  24036  minveclem6  24038  minveclem7  24039  mbfmulc2lem  24251  mbfmax  24253  mbfi1fseqlem4  24322  itg2gt0  24364  itg2cnlem2  24366  iblpos  24396  logbgt0b  25379  angrteqvd  25392  affineequiv  25409  affineequiv2  25410  dcubic  25432  rlimcnp  25551  rlimcnp2  25552  efexple  25865  bposlem7  25874  lgsabs1  25920  lgsquadlem1  25964  m1lgs  25972  lnhl  26409  colinearalg  26704  axcontlem2  26759  nbupgrel  27135  nb3grpr  27172  usgr0edg0rusgr  27365  isspthonpth  27538  rusgrnumwwlkl1  27754  eupth2lem3lem4  28016  minvecolem4  28663  minvecolem6  28665  minvecolem7  28666  hvmulcan2  28856  xppreima  30408  eqg0el  30977  smatrcl  31149  pstmxmet  31250  xrge0iifcnv  31286  ballotlemsima  31883  poimirlem27  35084  itg2addnclem  35108  itg2addnclem2  35109  iblabsnclem  35120  areacirclem2  35146  areacirclem4  35148  cvlcvrp  36636  ontric3g  40230  alephiso2  40257  sqrtcvallem1  40331  ntrclsk2  40771  ntrclsk13  40774  ntrneixb  40798  neicvgel1  40822  radcnvrat  41018  limsupmnflem  42362  logbge0b  44977  affinecomb2  45117  line2x  45168  itscnhlc0yqe  45173