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  570  2exeu  2111  eqtr2  2189  pm13.181  2422  rmob  3047  disjne  3468  seex  4320  tron  4367  fssres  5373  funbrfvb  5539  funopfvb  5540  fvelrnb  5544  fvco  5566  fvimacnvi  5610  ffvresb  5659  funresdfunsnss  5699  fvtp2g  5705  fvtp2  5708  fnex  5718  funex  5719  1st2nd  6160  dftpos4  6242  nnmsucr  6467  nnmcan  6498  xpmapenlem  6827  fundmfibi  6916  sup3exmid  8873  nzadd  9264  peano5uzti  9320  fnn0ind  9328  uztrn2  9504  irradd  9605  xltnegi  9792  xaddnemnf  9814  xaddnepnf  9815  xaddcom  9818  xnegdi  9825  elioore  9869  uzsubsubfz1  10004  fzo1fzo0n0  10139  elfzonelfzo  10186  qbtwnxr  10214  faclbnd  10675  faclbnd3  10677  dvdsprime  12076  pcgcd  12282  restuni  12966  stoig  12967  cnnei  13026  tgioo  13340  divcnap  13349  lgsdi  13732  bj-indind  13967