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  8215  addsubeq4  11521  muleqadd  11905  mulle0b  12137  adddivflid  13855  om2uzlti  13988  summodnegmod  16321  qnumdenbi  16778  dprdf11  20058  lvecvscan2  21132  mdetunilem9  22642  elfilss  23900  mbfmulc2lem  25696  itg2seq  25792  itg2cnlem2  25812  chpchtsum  27278  bposlem7  27349  lgsdilem  27383  lgsne0  27394  colhp  28793  axcontlem7  29000  pjnorm2  31756  cdj3lem1  32463  zringfrac  33562  ply1dg1rt  33584  zrhchr  33937  bj-gabima  36923  dochfln0  41460  mapdindp  41654  stgredgiun  47861