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  3107  eloprabga  6009  ereldm  6637  mapen  6907  ordiso2  7101  subcan  8281  conjmulap  8756  ltrec  8910  divelunit  10077  fseq1m1p1  10170  fzm1  10175  qsqeqor  10742  fihashneq0  10886  hashfacen  10928  cvg1nlemcau  11149  lenegsq  11260  dvdsmod  12027  bezoutlemle  12175  rpexp  12321  qnumdenbi  12360  eulerthlemh  12399  odzdvds  12414  pcelnn  12490  grpidpropdg  13017  sgrppropd  13056  mndpropd  13081  mhmpropd  13098  grppropd  13149  ghmnsgima  13398  cmnpropd  13425  qusecsub  13461  rngpropd  13511  ringpropd  13594  dvdsrpropdg  13703  resrhm2b  13805  lmodprop2d  13904  lsspropdg  13987  zndvds0  14206  bdxmet  14737  txmetcnp  14754  cnmet  14766  lgsne0  15279  lgsabs1  15280  gausslemma2dlem1a  15299  lgsquadlem2  15319