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  8232  addsubeq4  11551  muleqadd  11934  mulle0b  12166  adddivflid  13869  om2uzlti  14001  summodnegmod  16335  qnumdenbi  16791  dprdf11  20067  lvecvscan2  21137  mdetunilem9  22647  elfilss  23905  mbfmulc2lem  25701  itg2seq  25797  itg2cnlem2  25817  chpchtsum  27281  bposlem7  27352  lgsdilem  27386  lgsne0  27397  colhp  28796  axcontlem7  29003  pjnorm2  31759  cdj3lem1  32466  zringfrac  33547  ply1dg1rt  33569  zrhchr  33922  bj-gabima  36906  dochfln0  41434  mapdindp  41628