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  575  2exeu  2129  eqtr2  2207  pm13.181  2441  rmob  3069  disjne  3490  seex  4349  tron  4396  fssres  5405  funbrfvb  5573  funopfvb  5574  fvelrnb  5578  fvco  5601  fvimacnvi  5645  ffvresb  5694  funresdfunsnss  5734  fvtp2g  5740  fvtp2  5743  fnex  5753  funex  5754  1st2nd  6199  dftpos4  6281  nnmsucr  6506  nnmcan  6537  xpmapenlem  6866  fundmfibi  6955  sup3exmid  8931  nzadd  9322  peano5uzti  9378  fnn0ind  9386  uztrn2  9562  irradd  9663  xltnegi  9852  xaddnemnf  9874  xaddnepnf  9875  xaddcom  9878  xnegdi  9885  elioore  9929  uzsubsubfz1  10065  fzo1fzo0n0  10200  elfzonelfzo  10247  qbtwnxr  10275  faclbnd  10738  faclbnd3  10740  dvdsprime  12139  pcgcd  12345  restuni  14055  stoig  14056  cnnei  14115  tgioo  14429  divcnap  14438  lgsdi  14821  bj-indind  15067