Theorem sylanb 284

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 120	. 2 ⊢ (𝜑 → 𝜓)
3		sylanb.2	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	sylan 283	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 104   ↔ 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:  syl2anb  291  anabsan  577  2exeu  2172  eqtr2  2250  pm13.181  2485  rmob  3126  disjne  3550  seex  4438  tron  4485  fssres  5520  funbrfvb  5695  funopfvb  5696  fvelrnb  5702  fvco  5725  fvimacnvi  5770  ffvresb  5818  fcof  5841  funresdfunsnss  5865  fvtp2g  5871  fvtp2  5874  fnex  5884  funex  5887  1st2nd  6353  imacosuppfn  6446  dftpos4  6472  nnmsucr  6699  nnmcan  6730  xpmapenlem  7078  fundmfibi  7180  sup3exmid  9179  nzadd  9576  peano5uzti  9632  fnn0ind  9640  uztrn2  9818  irradd  9924  xltnegi  10114  xaddnemnf  10136  xaddnepnf  10137  xaddcom  10140  xnegdi  10147  elioore  10191  uzsubsubfz1  10328  fzo1fzo0n0  10468  elfzonelfzo  10521  qbtwnxr  10563  faclbnd  11049  faclbnd3  11051  swrdccat3b  11370  dvdsprime  12757  pcgcd  12965  znf1o  14730  restuni  14966  stoig  14967  cnnei  15026  tgioo  15348  divcnap  15359  ivthdich  15447  lgsdi  15839  bj-indind  16631