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 282	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4		3bitr2d.3	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
5	3, 4	bitrd 279	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:  raltpd  4786  opiota  8045  mapsnend  9036  adderpqlem  10949  mulerpqlem  10950  lesub2  11709  rec11  11912  fimaxre  12158  fiminre  12161  avglt1  12450  ixxun  13340  modmuladdnn0  13880  hashdom  14339  hashle00  14360  hashf1lem1  14415  hashf1lem1OLD  14416  swrdspsleq  14615  repsdf2  14728  2shfti  15027  mulre  15068  rlim  15439  rlim2  15440  modremain  16351  nn0seqcvgd  16507  divgcdcoprm0  16602  prmreclem6  16854  pwsleval  17439  issubc  17785  ismgmid  18584  grpsubeq0  18909  grpsubadd  18911  gastacos  19174  orbsta  19177  lsslss  20572  prmirredlem  21042  zndvds  21105  zntoslem  21112  cygznlem1  21122  islindf2  21369  ismhp3  21686  coe1mul2lem1  21789  restcld  22676  leordtvallem1  22714  leordtvallem2  22715  ist1-2  22851  xkoccn  23123  qtopcld  23217  ordthmeolem  23305  qustgpopn  23624  isxmet2d  23833  prdsxmetlem  23874  xblss2  23908  imasf1oxms  23998  neibl  24010  xrtgioo  24322  xrsxmet  24325  isncvsngp  24666  minveclem4  24949  minveclem6  24951  minveclem7  24952  mbfmulc2lem  25164  mbfmax  25166  mbfi1fseqlem4  25236  itg2gt0  25278  itg2cnlem2  25280  iblpos  25310  logbgt0b  26298  angrteqvd  26311  affineequiv  26328  affineequiv2  26329  dcubic  26351  rlimcnp  26470  rlimcnp2  26471  efexple  26784  bposlem7  26793  lgsabs1  26839  lgsquadlem1  26883  m1lgs  26891  subadds  27538  lnhl  27866  colinearalg  28168  axcontlem2  28223  nbupgrel  28602  nb3grpr  28639  usgr0edg0rusgr  28832  isspthonpth  29006  rusgrnumwwlkl1  29222  eupth2lem3lem4  29484  minvecolem4  30133  minvecolem6  30135  minvecolem7  30136  hvmulcan2  30326  xppreima  31871  eqg0el  32473  dvdsrspss  32491  ply1chr  32661  ply1degltel  32666  smatrcl  32776  pstmxmet  32877  xrge0iifcnv  32913  ballotlemsima  33514  poimirlem27  36515  itg2addnclem  36539  itg2addnclem2  36540  iblabsnclem  36551  areacirclem2  36577  areacirclem4  36579  cvlcvrp  38210  ontric3g  42273  alephiso2  42309  sqrtcvallem1  42382  ntrclsk2  42819  ntrclsk13  42822  ntrneixb  42846  neicvgel1  42870  radcnvrat  43073  limsupmnflem  44436  logbge0b  47249  affinecomb2  47389  line2x  47440  itscnhlc0yqe  47445