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  3164  eloprabga  6148  ereldm  6825  mapen  7112  ordiso2  7339  subcan  8545  conjmulap  9023  ltrec  9177  divelunit  10357  fseq1m1p1  10454  fzm1  10459  qsqeqor  11039  fihashneq0  11185  hashfacen  11236  ccat0  11312  cvg1nlemcau  11697  lenegsq  11808  dvdsmod  12576  bitsmod  12670  bezoutlemle  12732  rpexp  12878  qnumdenbi  12917  eulerthlemh  12956  odzdvds  12971  pcelnn  13047  ballotfilemfc0  13179  ballotfilemfcc  13180  grpidpropdg  13640  sgrppropd  13679  mndpropd  13704  mhmpropd  13724  grppropd  13775  ghmnsgima  14024  cmnpropd  14051  qusecsub  14087  rngpropd  14197  ringpropd  14284  dvdsrpropdg  14395  resrhm2b  14498  opprdrng  14561  lmodprop2d  14625  lsspropdg  14708  zndvds0  14927  bdxmet  15495  txmetcnp  15512  cnmet  15524  lgsne0  16040  lgsabs1  16041  gausslemma2dlem1a  16060  lgsquadlem2  16080  usgredg2v  16348  wlkeq  16478  eupth2lem3lem3fi  16594  eupth2lem3lem6fi  16595