Theorem 3bitr2rd 309

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 283	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4		3bitr2d.3	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
5	3, 4	bitr2d 281	1 ⊢ (𝜑 → (𝜏 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  fnsuppres  8131  addsubeq4  11399  muleqadd  11785  mulle0b  12018  adddivflid  13768  om2uzlti  13903  summodnegmod  16246  qnumdenbi  16705  dprdf11  19991  lvecvscan2  21105  mdetunilem9  22603  elfilss  23859  mbfmulc2lem  25632  itg2seq  25727  itg2cnlem2  25747  chpchtsum  27200  bposlem7  27271  lgsdilem  27305  lgsne0  27316  n0lts1e0  28378  colhp  28856  axcontlem7  29057  pjnorm2  31816  cdj3lem1  32523  receqid  32836  zringfrac  33637  ply1dg1rt  33663  zrhchr  34158  bj-gabima  37293  dochfln0  41969  mapdindp  42163  stgredgiun  48449