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  3149  eloprabga  6113  ereldm  6752  mapen  7037  ordiso2  7239  subcan  8439  conjmulap  8914  ltrec  9068  divelunit  10242  fseq1m1p1  10335  fzm1  10340  qsqeqor  10918  fihashneq0  11062  hashfacen  11106  ccat0  11182  cvg1nlemcau  11567  lenegsq  11678  dvdsmod  12446  bitsmod  12540  bezoutlemle  12602  rpexp  12748  qnumdenbi  12787  eulerthlemh  12826  odzdvds  12841  pcelnn  12917  grpidpropdg  13480  sgrppropd  13519  mndpropd  13546  mhmpropd  13572  grppropd  13623  ghmnsgima  13878  cmnpropd  13905  qusecsub  13941  rngpropd  13992  ringpropd  14075  dvdsrpropdg  14185  resrhm2b  14287  lmodprop2d  14386  lsspropdg  14469  zndvds0  14688  bdxmet  15254  txmetcnp  15271  cnmet  15283  lgsne0  15796  lgsabs1  15797  gausslemma2dlem1a  15816  lgsquadlem2  15836  usgredg2v  16104  wlkeq  16234  eupth2lem3lem3fi  16350  eupth2lem3lem6fi  16351