Theorem 3bitr3d 217

Description: Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 24-Apr-1996.)

Hypotheses

Ref	Expression
3bitr3d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
3bitr3d.2	⊢ (𝜑 → (𝜓 ↔ 𝜃))
3bitr3d.3	⊢ (𝜑 → (𝜒 ↔ 𝜏))

Assertion

Ref	Expression
3bitr3d	⊢ (𝜑 → (𝜃 ↔ 𝜏))

Proof of Theorem 3bitr3d

Step	Hyp	Ref	Expression
1		3bitr3d.2	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
2		3bitr3d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	bitr3d 189	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
4		3bitr3d.3	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜏))
5	3, 4	bitrd 187	1 ⊢ (𝜑 → (𝜃 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  csbcomg  3072  eloprabga  5938  ereldm  6553  mapen  6821  ordiso2  7009  subcan  8163  conjmulap  8635  ltrec  8788  divelunit  9948  fseq1m1p1  10040  fzm1  10045  qsqeqor  10575  fihashneq0  10718  hashfacen  10760  cvg1nlemcau  10937  lenegsq  11048  dvdsmod  11811  bezoutlemle  11952  rpexp  12096  qnumdenbi  12135  eulerthlemh  12174  odzdvds  12188  pcelnn  12263  grpidpropdg  12617  mndpropd  12665  mhmpropd  12678  grppropd  12713  bdxmet  13256  txmetcnp  13273  cnmet  13285  lgsne0  13694  lgsabs1  13695