Theorem 3bitr2rd 308

Description: Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)

Hypotheses

Ref	Expression
3bitr2d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
3bitr2d.2	⊢ (𝜑 → (𝜃 ↔ 𝜒))
3bitr2d.3	⊢ (𝜑 → (𝜃 ↔ 𝜏))

Assertion

Ref	Expression
3bitr2rd	⊢ (𝜑 → (𝜏 ↔ 𝜓))

Proof of Theorem 3bitr2rd

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	bitr2d 280	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:  fnsuppres  8141  addsubeq4  11408  muleqadd  11794  mulle0b  12027  adddivflid  13777  om2uzlti  13912  summodnegmod  16255  qnumdenbi  16714  dprdf11  20000  lvecvscan2  21110  mdetunilem9  22585  elfilss  23841  mbfmulc2lem  25614  itg2seq  25709  itg2cnlem2  25729  chpchtsum  27182  bposlem7  27253  lgsdilem  27287  lgsne0  27298  n0lts1e0  28360  colhp  28838  axcontlem7  29039  pjnorm2  31798  cdj3lem1  32505  receqid  32817  zringfrac  33614  ply1dg1rt  33640  zrhchr  34118  bj-gabima  37247  dochfln0  41923  mapdindp  42117  stgredgiun  48434