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  8116  addsubeq4  11370  muleqadd  11756  mulle0b  11988  adddivflid  13717  om2uzlti  13852  summodnegmod  16192  qnumdenbi  16650  dprdf11  19932  lvecvscan2  21044  mdetunilem9  22530  elfilss  23786  mbfmulc2lem  25570  itg2seq  25665  itg2cnlem2  25685  chpchtsum  27152  bposlem7  27223  lgsdilem  27257  lgsne0  27268  colhp  28743  axcontlem7  28943  pjnorm2  31699  cdj3lem1  32406  receqid  32720  zringfrac  33511  ply1dg1rt  33535  zrhchr  33979  bj-gabima  36974  dochfln0  41516  mapdindp  41710  stgredgiun  47989