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  8188  addsubeq4  11495  muleqadd  11879  mulle0b  12111  adddivflid  13833  om2uzlti  13966  summodnegmod  16304  qnumdenbi  16761  dprdf11  20004  lvecvscan2  21071  mdetunilem9  22556  elfilss  23812  mbfmulc2lem  25598  itg2seq  25693  itg2cnlem2  25713  chpchtsum  27180  bposlem7  27251  lgsdilem  27285  lgsne0  27296  colhp  28695  axcontlem7  28895  pjnorm2  31654  cdj3lem1  32361  receqid  32668  zringfrac  33515  ply1dg1rt  33538  zrhchr  33951  bj-gabima  36904  dochfln0  41442  mapdindp  41636  stgredgiun  47918