Theorem 3bitr2rd 311

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 285	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4		3bitr2d.3	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
5	3, 4	bitr2d 283	1 ⊢ (𝜑 → (𝜏 ↔ 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  fnsuppres  8212  addsubeq4  11576  muleqadd  11964  mulle0b  12192  adddivflid  13962  om2uzlti  14097  summodnegmod  16462  qnumdenbi  16926  dprdf11  20245  lvecvscan2  21396  mdetunilem9  22941  elfilss  24201  mbfmulc2lem  25974  itg2seq  26069  itg2cnlem2  26089  chpchtsum  27552  bposlem7  27623  lgsdilem  27657  lgsne0  27668  n0lts1e0  28760  colhp  29254  axcontlem7  29554  pjnorm2  32335  cdj3lem1  33042  receqid  33383  rlocisunit  33884  zringfrac  34133  ply1dg1rt  34159  zrhchr  34653  bj-gabima  37946  dochfln0  42628  mapdindp  42822  stgredgiun  49150