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  3127  eloprabga  6062  ereldm  6695  mapen  6975  ordiso2  7170  subcan  8369  conjmulap  8844  ltrec  8998  divelunit  10166  fseq1m1p1  10259  fzm1  10264  qsqeqor  10839  fihashneq0  10983  hashfacen  11025  ccat0  11097  cvg1nlemcau  11461  lenegsq  11572  dvdsmod  12339  bitsmod  12433  bezoutlemle  12495  rpexp  12641  qnumdenbi  12680  eulerthlemh  12719  odzdvds  12734  pcelnn  12810  grpidpropdg  13373  sgrppropd  13412  mndpropd  13439  mhmpropd  13465  grppropd  13516  ghmnsgima  13771  cmnpropd  13798  qusecsub  13834  rngpropd  13884  ringpropd  13967  dvdsrpropdg  14076  resrhm2b  14178  lmodprop2d  14277  lsspropdg  14360  zndvds0  14579  bdxmet  15140  txmetcnp  15157  cnmet  15169  lgsne0  15682  lgsabs1  15683  gausslemma2dlem1a  15702  lgsquadlem2  15722  usgredg2v  15987