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 206

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 207

This theorem is referenced by:  raltpd  4785  opiota  8082  mapsnend  9074  adderpqlem  10991  mulerpqlem  10992  lesub2  11755  rec11  11962  fimaxre  12209  fiminre  12212  avglt1  12501  ixxun  13399  modmuladdnn0  13952  hashdom  14414  hashle00  14435  hashf1lem1  14490  swrdspsleq  14699  repsdf2  14812  2shfti  15115  mulre  15156  rlim  15527  rlim2  15528  modremain  16441  nn0seqcvgd  16603  divgcdcoprm0  16698  prmreclem6  16954  pwsleval  17539  issubc  17885  ismgmid  18690  grpsubeq0  19056  grpsubadd  19058  eqg0el  19213  gastacos  19340  orbsta  19343  lsslss  20976  prmirredlem  21500  zndvds  21585  zntoslem  21592  cygznlem1  21602  islindf2  21851  ismhp3  22163  coe1mul2lem1  22285  ply1chr  22325  restcld  23195  leordtvallem1  23233  leordtvallem2  23234  ist1-2  23370  xkoccn  23642  qtopcld  23736  ordthmeolem  23824  qustgpopn  24143  isxmet2d  24352  prdsxmetlem  24393  xblss2  24427  imasf1oxms  24517  neibl  24529  xrtgioo  24841  xrsxmet  24844  isncvsngp  25196  minveclem4  25479  minveclem6  25481  minveclem7  25482  mbfmulc2lem  25695  mbfmax  25697  mbfi1fseqlem4  25767  itg2gt0  25809  itg2cnlem2  25811  iblpos  25842  r1pid2  26215  logbgt0b  26850  angrteqvd  26863  affineequiv  26880  affineequiv2  26881  dcubic  26903  rlimcnp  27022  rlimcnp2  27023  efexple  27339  bposlem7  27348  lgsabs1  27394  lgsquadlem1  27438  m1lgs  27446  subadds  28114  lnhl  28637  colinearalg  28939  axcontlem2  28994  nbupgrel  29376  nb3grpr  29413  usgr0edg0rusgr  29607  isspthonpth  29781  rusgrnumwwlkl1  29997  eupth2lem3lem4  30259  minvecolem4  30908  minvecolem6  30910  minvecolem7  30911  hvmulcan2  31101  xppreima  32661  fzo0opth  32812  fracerl  33287  dvdsrspss  33394  ply1degltel  33594  r1pid2OLD  33608  smatrcl  33756  pstmxmet  33857  xrge0iifcnv  33893  ballotlemsima  34496  poimirlem27  37633  itg2addnclem  37657  itg2addnclem2  37658  iblabsnclem  37669  areacirclem2  37695  areacirclem4  37697  cvlcvrp  39321  ontric3g  43511  alephiso2  43547  sqrtcvallem1  43620  ntrclsk2  44057  ntrclsk13  44060  ntrneixb  44084  neicvgel1  44108  radcnvrat  44309  limsupmnflem  45675  dfvopnbgr2  47776  logbge0b  48412  affinecomb2  48552  line2x  48603  itscnhlc0yqe  48608