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  6178  ereldm  6856  mapen  7150  ordiso2  7381  subcan  8588  conjmulap  9067  ltrec  9221  divelunit  10421  fseq1m1p1  10519  fzm1  10524  qsqeqor  11108  fihashneq0  11255  hashfacen  11306  hashf1  11309  ccat0  11386  cvg1nlemcau  11772  lenegsq  11884  dvdsmod  12654  bitsmod  12748  bezoutlemle  12810  rpexp  12957  qnumdenbi  12997  eulerthlemh  13038  odzdvds  13053  pcelnn  13129  ballotfilemfc0  13290  ballotfilemfcc  13291  grpidpropdg  13753  sgrppropd  13787  mndpropd  13812  mhmpropd  13832  grppropd  13881  ghmnsgima  14130  cmnpropd  14188  qusecsub  14225  rngpropd  14361  ringpropd  14450  dvdsrpropdg  14563  resrhm2b  14666  opprdrng  14729  lmodprop2d  14794  lsspropdg  14877  zndvds0  15094  assapropd  15123  bdxmet  15724  txmetcnp  15741  cnmet  15753  birthdaylem3  16224  bposlem7  16314  lgsne0  16359  lgsabs1  16360  gausslemma2dlem1a  16379  lgsquadlem2  16399  usgredg2v  16667  wlkeq  16797  eupth2lem3lem3fi  16913  eupth2lem3lem6fi  16914