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  8134  addsubeq4  11399  muleqadd  11785  mulle0b  12018  adddivflid  13768  om2uzlti  13903  summodnegmod  16246  qnumdenbi  16705  dprdf11  19991  lvecvscan2  21102  mdetunilem9  22595  elfilss  23851  mbfmulc2lem  25624  itg2seq  25719  itg2cnlem2  25739  chpchtsum  27196  bposlem7  27267  lgsdilem  27301  lgsne0  27312  n0lts1e0  28374  colhp  28852  axcontlem7  29053  pjnorm2  31813  cdj3lem1  32520  receqid  32832  zringfrac  33629  ply1dg1rt  33655  zrhchr  34134  bj-gabima  37263  dochfln0  41937  mapdindp  42131  stgredgiun  48446