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  3150  eloprabga  6108  ereldm  6747  mapen  7032  ordiso2  7234  subcan  8434  conjmulap  8909  ltrec  9063  divelunit  10237  fseq1m1p1  10330  fzm1  10335  qsqeqor  10913  fihashneq0  11057  hashfacen  11101  ccat0  11174  cvg1nlemcau  11546  lenegsq  11657  dvdsmod  12425  bitsmod  12519  bezoutlemle  12581  rpexp  12727  qnumdenbi  12766  eulerthlemh  12805  odzdvds  12820  pcelnn  12896  grpidpropdg  13459  sgrppropd  13498  mndpropd  13525  mhmpropd  13551  grppropd  13602  ghmnsgima  13857  cmnpropd  13884  qusecsub  13920  rngpropd  13971  ringpropd  14054  dvdsrpropdg  14164  resrhm2b  14266  lmodprop2d  14365  lsspropdg  14448  zndvds0  14667  bdxmet  15228  txmetcnp  15245  cnmet  15257  lgsne0  15770  lgsabs1  15771  gausslemma2dlem1a  15790  lgsquadlem2  15810  usgredg2v  16078  wlkeq  16208  eupth2lem3lem3fi  16324  eupth2lem3lem6fi  16325