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  5940  ereldm  6556  mapen  6824  ordiso2  7012  subcan  8174  conjmulap  8646  ltrec  8799  divelunit  9959  fseq1m1p1  10051  fzm1  10056  qsqeqor  10586  fihashneq0  10729  hashfacen  10771  cvg1nlemcau  10948  lenegsq  11059  dvdsmod  11822  bezoutlemle  11963  rpexp  12107  qnumdenbi  12146  eulerthlemh  12185  odzdvds  12199  pcelnn  12274  grpidpropdg  12628  mndpropd  12676  mhmpropd  12689  grppropd  12724  bdxmet  13295  txmetcnp  13312  cnmet  13324  lgsne0  13733  lgsabs1  13734