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  3117  eloprabga  6039  ereldm  6672  mapen  6950  ordiso2  7144  subcan  8334  conjmulap  8809  ltrec  8963  divelunit  10131  fseq1m1p1  10224  fzm1  10229  qsqeqor  10802  fihashneq0  10946  hashfacen  10988  ccat0  11060  cvg1nlemcau  11339  lenegsq  11450  dvdsmod  12217  bitsmod  12311  bezoutlemle  12373  rpexp  12519  qnumdenbi  12558  eulerthlemh  12597  odzdvds  12612  pcelnn  12688  grpidpropdg  13250  sgrppropd  13289  mndpropd  13316  mhmpropd  13342  grppropd  13393  ghmnsgima  13648  cmnpropd  13675  qusecsub  13711  rngpropd  13761  ringpropd  13844  dvdsrpropdg  13953  resrhm2b  14055  lmodprop2d  14154  lsspropdg  14237  zndvds0  14456  bdxmet  15017  txmetcnp  15034  cnmet  15046  lgsne0  15559  lgsabs1  15560  gausslemma2dlem1a  15579  lgsquadlem2  15599