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  8147  addsubeq4  11412  muleqadd  11798  mulle0b  12030  adddivflid  13756  om2uzlti  13891  summodnegmod  16232  qnumdenbi  16690  dprdf11  19931  lvecvscan2  20998  mdetunilem9  22483  elfilss  23739  mbfmulc2lem  25524  itg2seq  25619  itg2cnlem2  25639  chpchtsum  27106  bposlem7  27177  lgsdilem  27211  lgsne0  27222  colhp  28673  axcontlem7  28873  pjnorm2  31629  cdj3lem1  32336  receqid  32641  zringfrac  33498  ply1dg1rt  33521  zrhchr  33937  bj-gabima  36901  dochfln0  41444  mapdindp  41638  stgredgiun  47930