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  4726  opiota  8005  mapsnend  8976  adderpqlem  10868  mulerpqlem  10869  lesub2  11636  rec11  11844  fimaxre  12091  fiminre  12094  avglt1  12406  ixxun  13305  modmuladdnn0  13868  hashdom  14332  hashle00  14353  hashf1lem1  14408  swrdspsleq  14619  repsdf2  14731  2shfti  15033  mulre  15074  rlim  15448  rlim2  15449  modremain  16368  nn0seqcvgd  16530  divgcdcoprm0  16625  prmreclem6  16883  pwsleval  17448  issubc  17793  ismgmid  18624  grpsubeq0  18993  grpsubadd  18995  eqg0el  19149  gastacos  19276  orbsta  19279  lsslss  20947  prmirredlem  21462  zndvds  21539  zntoslem  21546  cygznlem1  21556  islindf2  21804  ismhp3  22118  coe1mul2lem1  22242  ply1chr  22281  restcld  23147  leordtvallem1  23185  leordtvallem2  23186  ist1-2  23322  xkoccn  23594  qtopcld  23688  ordthmeolem  23776  qustgpopn  24095  isxmet2d  24302  prdsxmetlem  24343  xblss2  24377  imasf1oxms  24464  neibl  24476  xrtgioo  24782  xrsxmet  24785  isncvsngp  25126  minveclem4  25409  minveclem6  25411  minveclem7  25412  mbfmulc2lem  25624  mbfmax  25626  mbfi1fseqlem4  25695  itg2gt0  25737  itg2cnlem2  25739  iblpos  25770  r1pid2  26137  logbgt0b  26770  angrteqvd  26783  affineequiv  26800  affineequiv2  26801  dcubic  26823  rlimcnp  26942  rlimcnp2  26943  efexple  27258  bposlem7  27267  lgsabs1  27313  lgsquadlem1  27357  m1lgs  27365  subadds  28076  lnhl  28697  colinearalg  28993  axcontlem2  29048  nbupgrel  29428  nb3grpr  29465  usgr0edg0rusgr  29659  isspthonpth  29832  rusgrnumwwlkl1  30054  eupth2lem3lem4  30316  minvecolem4  30966  minvecolem6  30968  minvecolem7  30969  hvmulcan2  31159  xppreima  32733  fzo0opth  32891  fracerl  33382  dvdsrspss  33462  ply1degltel  33669  r1pid2OLD  33684  psrbasfsupp  33687  smatrcl  33956  pstmxmet  34057  xrge0iifcnv  34093  ballotlemsima  34676  poimirlem27  37982  itg2addnclem  38006  itg2addnclem2  38007  iblabsnclem  38018  areacirclem2  38044  areacirclem4  38046  cvlcvrp  39800  ontric3g  43967  alephiso2  44003  sqrtcvallem1  44076  ntrclsk2  44513  ntrclsk13  44516  ntrneixb  44540  neicvgel1  44564  radcnvrat  44759  limsupmnflem  46166  chnsubseqwl  47325  nprmmul1  47999  dfvopnbgr2  48341  pgnbgreunbgrlem2lem1  48602  pgnbgreunbgrlem2lem2  48603  logbge0b  49051  affinecomb2  49191  line2x  49242  itscnhlc0yqe  49247