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  8143  addsubeq4  11407  muleqadd  11793  mulle0b  12025  adddivflid  13750  om2uzlti  13885  summodnegmod  16225  qnumdenbi  16683  dprdf11  19966  lvecvscan2  21079  mdetunilem9  22576  elfilss  23832  mbfmulc2lem  25616  itg2seq  25711  itg2cnlem2  25731  chpchtsum  27198  bposlem7  27269  lgsdilem  27303  lgsne0  27314  n0lts1e0  28376  colhp  28854  axcontlem7  29055  pjnorm2  31815  cdj3lem1  32522  receqid  32835  zringfrac  33647  ply1dg1rt  33673  zrhchr  34152  bj-gabima  37188  dochfln0  41853  mapdindp  42047  stgredgiun  48318