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  4752  opiota  8065  mapsnend  9043  adderpqlem  10957  mulerpqlem  10958  lesub2  11727  rec11  11931  fimaxre  12177  fiminre  12180  avglt1  12500  ixxun  13406  modmuladdnn0  13971  hashdom  14435  hashle00  14456  hashf1lem1  14512  swrdspsleq  14727  repsdf2  14841  2shfti  15143  mulre  15198  rlim  15572  rlim2  15573  modremain  16491  nn0seqcvgd  16653  divgcdcoprm0  16748  prmreclem6  17006  pwsleval  17572  issubc  17917  ismgmid  18748  grpsubeq0  19123  grpsubadd  19125  eqg0el  19285  gastacos  19411  orbsta  19414  lsslss  21119  prmirredlem  21659  zndvds  21736  zntoslem  21743  cygznlem1  21753  islindf2  22001  ismhp3  22342  coe1mul2lem1  22465  ply1chr  22503  restcld  23366  leordtvallem1  23404  leordtvallem2  23405  ist1-2  23541  xkoccn  23813  qtopcld  23907  ordthmeolem  23995  qustgpopn  24314  isxmet2d  24521  prdsxmetlem  24562  xblss2  24596  imasf1oxms  24683  neibl  24695  xrtgioo  25001  xrsxmet  25004  isncvsngp  25345  minveclem4  25628  minveclem6  25630  minveclem7  25631  mbfmulc2lem  25843  mbfmax  25845  mbfi1fseqlem4  25914  itg2gt0  25956  itg2cnlem2  25958  iblpos  25989  r1pid2  26356  logbgt0b  26995  angrteqvd  27008  affineequiv  27025  affineequiv2  27026  dcubic  27048  rlimcnp  27167  rlimcnp2  27168  efexple  27482  bposlem7  27491  lgsabs1  27537  lgsquadlem1  27581  m1lgs  27589  subadds  28300  lnhl  28924  elplng  29099  colinearalg  29297  axcontlem2  29352  nbupgrel  29732  nb3grpr  29769  usgr0edg0rusgr  29962  isspthonpth  30135  rusgrnumwwlkl1  30357  eupth2lem3lem4  30619  minvecolem4  31269  minvecolem6  31271  minvecolem7  31272  hvmulcan2  31462  xppreima  33027  fzo0opth  33185  fracerl  33658  dvdsrspss  33731  ply1degltel  33915  psrbasfsupp  33932  smatrcl  34217  pstmxmet  34318  xrge0iifcnv  34354  ballotlemsima  34938  poimirlem27  38339  itg2addnclem  38363  itg2addnclem2  38364  iblabsnclem  38375  areacirclem2  38401  areacirclem4  38403  cvlcvrp  40155  ontric3g  44289  alephiso2  44325  sqrtcvallem1  44398  ntrclsk2  44835  ntrclsk13  44838  ntrneixb  44862  neicvgel1  44886  radcnvrat  45065  limsupmnflem  46475  chnsubseqwl  47636  nprmmul1  48317  dfvopnbgr2  48659  pgnbgreunbgrlem2lem1  48920  pgnbgreunbgrlem2lem2  48921  logbge0b  49384  affinecomb2  49524  line2x  49575  itscnhlc0yqe  49580