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  8216  addsubeq4  11523  muleqadd  11907  mulle0b  12139  adddivflid  13858  om2uzlti  13991  summodnegmod  16324  qnumdenbi  16781  dprdf11  20043  lvecvscan2  21114  mdetunilem9  22626  elfilss  23884  mbfmulc2lem  25682  itg2seq  25777  itg2cnlem2  25797  chpchtsum  27263  bposlem7  27334  lgsdilem  27368  lgsne0  27379  colhp  28778  axcontlem7  28985  pjnorm2  31746  cdj3lem1  32453  zringfrac  33582  ply1dg1rt  33604  zrhchr  33975  bj-gabima  36941  dochfln0  41479  mapdindp  41673  stgredgiun  47925