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 ⊢ (𝜑 → (𝜃 ↔ 𝜏))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  csbcomg  3170  eloprabga  6175  ereldm  6852  mapen  7146  ordiso2  7375  subcan  8581  conjmulap  9060  ltrec  9214  divelunit  10406  fseq1m1p1  10504  fzm1  10509  qsqeqor  11089  fihashneq0  11235  hashfacen  11286  hashf1  11289  ccat0  11366  cvg1nlemcau  11752  lenegsq  11863  dvdsmod  12631  bitsmod  12725  bezoutlemle  12787  rpexp  12933  qnumdenbi  12972  eulerthlemh  13011  odzdvds  13026  pcelnn  13102  ballotfilemfc0  13234  ballotfilemfcc  13235  grpidpropdg  13696  sgrppropd  13730  mndpropd  13755  mhmpropd  13775  grppropd  13824  ghmnsgima  14073  cmnpropd  14100  qusecsub  14137  rngpropd  14256  ringpropd  14345  dvdsrpropdg  14456  resrhm2b  14559  opprdrng  14622  lmodprop2d  14687  lsspropdg  14770  zndvds0  14987  assapropd  15016  bdxmet  15604  txmetcnp  15621  cnmet  15633  birthdaylem3  16095  lgsne0  16169  lgsabs1  16170  gausslemma2dlem1a  16189  lgsquadlem2  16209  usgredg2v  16477  wlkeq  16607  eupth2lem3lem3fi  16723  eupth2lem3lem6fi  16724