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 205

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 206

This theorem is referenced by:  fnsuppres  8038  addsubeq4  11286  muleqadd  11669  mulle0b  11896  adddivflid  13588  om2uzlti  13720  summodnegmod  16045  qnumdenbi  16497  dprdf11  19675  lvecvscan2  20423  mdetunilem9  21818  elfilss  23076  mbfmulc2lem  24860  itg2seq  24956  itg2cnlem2  24976  chpchtsum  26416  bposlem7  26487  lgsdilem  26521  lgsne0  26532  colhp  27180  axcontlem7  27387  pjnorm2  30138  cdj3lem1  30845  zrhchr  31975  bj-gabima  35176  dochfln0  39691  mapdindp  39885