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  8133  addsubeq4  11395  muleqadd  11781  mulle0b  12013  adddivflid  13738  om2uzlti  13873  summodnegmod  16213  qnumdenbi  16671  dprdf11  19954  lvecvscan2  21067  mdetunilem9  22564  elfilss  23820  mbfmulc2lem  25604  itg2seq  25699  itg2cnlem2  25719  chpchtsum  27186  bposlem7  27257  lgsdilem  27291  lgsne0  27302  n0lts1e0  28364  colhp  28842  axcontlem7  29043  pjnorm2  31802  cdj3lem1  32509  receqid  32824  zringfrac  33635  ply1dg1rt  33661  zrhchr  34131  bj-gabima  37141  dochfln0  41737  mapdindp  41931  stgredgiun  48204