Theorem 3bitr2d 295

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

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  ceqsralt  3202  raltpd  4258  opiota  7118  adderpqlem  9655  mulerpqlem  9656  lesub2  10402  rec11  10602  avglt1  11147  ixxun  12062  modmuladdnn0  12576  hashdom  13029  hashle00  13049  hashf1lem1  13096  swrdspsleq  13301  repsdf2  13376  2shfti  13668  mulre  13709  rlim  14074  rlim2  14075  modremain  14970  nn0seqcvgd  15121  divgcdcoprm0  15217  prmreclem6  15463  pwsleval  15976  issubc  16318  ismgmid  17087  grpsubeq0  17324  grpsubadd  17326  gastacos  17566  orbsta  17569  lsslss  18782  coe1mul2lem1  19458  prmirredlem  19660  zndvds  19717  zntoslem  19724  cygznlem1  19734  islindf2  19972  restcld  20786  leordtvallem1  20824  leordtvallem2  20825  ist1-2  20961  xkoccn  21232  qtopcld  21326  ordthmeolem  21414  qustgpopn  21733  isxmet2d  21942  prdsxmetlem  21983  xblss2  22017  imasf1oxms  22104  neibl  22116  xrtgioo  22417  xrsxmet  22420  isncvsngp  22757  minveclem4  23011  minveclem6  23013  minveclem7  23014  mbfmulc2lem  23220  mbfmax  23222  mbfi1fseqlem4  23291  itg2gt0  23333  itg2cnlem2  23335  iblpos  23365  angrteqvd  24336  affineequiv  24353  affineequiv2  24354  dcubic  24373  rlimcnp  24492  rlimcnp2  24493  efexple  24806  bposlem7  24815  lgsabs1  24861  lgsquadlem1  24905  m1lgs  24913  lnhl  25310  colinearalg  25590  axcontlem2  25645  nb3grapr  25982  el2wlksotot  26409  rusgranumwlkl1  26474  numclwlk1lem2f1  26621  minvecolem4  27120  minvecolem6  27122  minvecolem7  27123  hvmulcan2  27314  xppreima  28829  smatrcl  29190  pstmxmet  29268  xrge0iifcnv  29307  ballotlemsima  29904  poimirlem27  32606  itg2addnclem  32631  itg2addnclem2  32632  iblabsnclem  32643  areacirclem2  32671  areacirclem4  32673  cvlcvrp  33645  ntrclsk2  37386  ntrclsk13  37389  ntrneixb  37413  neicvgel1  37437  radcnvrat  37535  mapsnend  38386  nbupgrel  40567  nb3grpr  40610  usgr0edg0rusgr  40775  isspthonpth-av  40955  rusgrnumwwlkl1  41172  eupth2lem3lem4  41399  av-numclwlk1lem2f1  41524  logbge0b  42155