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  7151  ordiso2  7382  subcan  8589  conjmulap  9068  ltrec  9222  divelunit  10422  fseq1m1p1  10520  fzm1  10525  qsqeqor  11109  fihashneq0  11256  hashfacen  11307  hashf1  11310  ccat0  11387  cvg1nlemcau  11773  lenegsq  11885  dvdsmod  12655  bitsmod  12749  bezoutlemle  12811  rpexp  12958  qnumdenbi  12998  eulerthlemh  13039  odzdvds  13054  pcelnn  13130  ballotfilemfc0  13291  ballotfilemfcc  13292  grpidpropdg  13754  sgrppropd  13788  mndpropd  13813  mhmpropd  13833  grppropd  13882  ghmnsgima  14131  cmnpropd  14189  qusecsub  14226  rngpropd  14362  ringpropd  14451  dvdsrpropdg  14564  resrhm2b  14667  opprdrng  14730  lmodprop2d  14795  lsspropdg  14878  zndvds0  15095  assapropd  15124  bdxmet  15739  txmetcnp  15756  cnmet  15768  birthdaylem3  16239  bposlem7  16329  lgsne0  16374  lgsabs1  16375  gausslemma2dlem1a  16394  lgsquadlem2  16414  usgredg2v  16682  wlkeq  16812  eupth2lem3lem3fi  16928  eupth2lem3lem6fi  16929