Theorem 3bitr3d 218

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 190	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
4		3bitr3d.3	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜏))
5	3, 4	bitrd 188	1 ⊢ (𝜑 → (𝜃 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  csbcomg  3080  eloprabga  5961  ereldm  6577  mapen  6845  ordiso2  7033  subcan  8211  conjmulap  8685  ltrec  8839  divelunit  10001  fseq1m1p1  10094  fzm1  10099  qsqeqor  10630  fihashneq0  10773  hashfacen  10815  cvg1nlemcau  10992  lenegsq  11103  dvdsmod  11867  bezoutlemle  12008  rpexp  12152  qnumdenbi  12191  eulerthlemh  12230  odzdvds  12244  pcelnn  12319  grpidpropdg  12792  mndpropd  12840  mhmpropd  12856  grppropd  12892  cmnpropd  13096  ringpropd  13215  dvdsrpropdg  13314  bdxmet  13971  txmetcnp  13988  cnmet  14000  lgsne0  14409  lgsabs1  14410