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  8178  addsubeq4  11477  muleqadd  11860  mulle0b  12087  adddivflid  13785  om2uzlti  13917  summodnegmod  16232  qnumdenbi  16682  dprdf11  19895  lvecvscan2  20731  mdetunilem9  22129  elfilss  23387  mbfmulc2lem  25171  itg2seq  25267  itg2cnlem2  25287  chpchtsum  26729  bposlem7  26800  lgsdilem  26834  lgsne0  26845  colhp  28059  axcontlem7  28266  pjnorm2  31018  cdj3lem1  31725  zrhchr  33025  bj-gabima  35906  dochfln0  40434  mapdindp  40628