Theorem 3bitr2rd 310

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  fnsuppres  8165  addsubeq4  11439  muleqadd  11825  mulle0b  12057  adddivflid  13822  om2uzlti  13957  summodnegmod  16311  qnumdenbi  16770  dprdf11  20056  lvecvscan2  21170  mdetunilem9  22668  elfilss  23924  mbfmulc2lem  25697  itg2seq  25792  itg2cnlem2  25812  chpchtsum  27271  bposlem7  27342  lgsdilem  27376  lgsne0  27387  n0lts1e0  28449  colhp  28927  axcontlem7  29128  pjnorm2  31887  cdj3lem1  32594  receqid  32907  rlocisunit  33418  zringfrac  33711  ply1dg1rt  33737  zrhchr  34232  bj-gabima  37386  dochfln0  42062  mapdindp  42256  stgredgiun  48541