Theorem 3bitr2rd 307

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 281	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4		3bitr2d.3	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
5	3, 4	bitr2d 279	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  7991  addsubeq4  11219  muleqadd  11602  mulle0b  11829  adddivflid  13519  om2uzlti  13651  summodnegmod  15977  qnumdenbi  16429  dprdf11  19607  lvecvscan2  20355  mdetunilem9  21750  elfilss  23008  mbfmulc2lem  24792  itg2seq  24888  itg2cnlem2  24908  chpchtsum  26348  bposlem7  26419  lgsdilem  26453  lgsne0  26464  colhp  27112  axcontlem7  27319  pjnorm2  30068  cdj3lem1  30775  zrhchr  31905  bj-gabima  35107  dochfln0  39470  mapdindp  39664