Theorem sylanb 282

Description: A syllogism inference. (Contributed by NM, 18-May-1994.)

Hypotheses

Ref	Expression
sylanb.1	⊢ (𝜑 ↔ 𝜓)
sylanb.2	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
sylanb	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Proof of Theorem sylanb

Step	Hyp	Ref	Expression
1		sylanb.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	biimpi 119	. 2 ⊢ (𝜑 → 𝜓)
3		sylanb.2	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	sylan 281	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  syl2anb  289  anabsan  565  2exeu  2092  eqtr2  2159  pm13.181  2391  rmob  3005  disjne  3421  seex  4265  tron  4312  fssres  5306  funbrfvb  5472  funopfvb  5473  fvelrnb  5477  fvco  5499  fvimacnvi  5542  ffvresb  5591  funresdfunsnss  5631  fvtp2g  5637  fvtp2  5640  fnex  5650  funex  5651  1st2nd  6087  dftpos4  6168  nnmsucr  6392  nnmcan  6423  xpmapenlem  6751  fundmfibi  6835  sup3exmid  8739  nzadd  9130  peano5uzti  9183  fnn0ind  9191  uztrn2  9367  irradd  9465  xltnegi  9648  xaddnemnf  9670  xaddnepnf  9671  xaddcom  9674  xnegdi  9681  elioore  9725  uzsubsubfz1  9859  fzo1fzo0n0  9991  elfzonelfzo  10038  qbtwnxr  10066  faclbnd  10519  faclbnd3  10521  dvdsprime  11839  restuni  12380  stoig  12381  cnnei  12440  tgioo  12754  divcnap  12763  bj-indind  13301