Theorem 3bitr2rd 310

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  fnsuppres  7857  addsubeq4  10901  muleqadd  11284  mulle0b  11511  adddivflid  13189  om2uzlti  13319  summodnegmod  15640  qnumdenbi  16084  dprdf11  19145  lvecvscan2  19884  mdetunilem9  21229  elfilss  22484  mbfmulc2lem  24248  itg2seq  24343  itg2cnlem2  24363  chpchtsum  25795  bposlem7  25866  lgsdilem  25900  lgsne0  25911  colhp  26556  axcontlem7  26756  pjnorm2  29504  cdj3lem1  30211  zrhchr  31217  dochfln0  38628  mapdindp  38822