Theorem sylanb 279

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 278	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  syl2anb  286  anabsan  543  2exeu  2047  eqtr2  2113  pm13.181  2344  rmob  2945  disjne  3355  seex  4186  tron  4233  fssres  5221  funbrfvb  5382  funopfvb  5383  fvelrnb  5387  fvco  5409  fvimacnvi  5452  ffvresb  5500  funresdfunsnss  5539  fvtp2g  5545  fvtp2  5548  fnex  5558  funex  5559  1st2nd  5989  dftpos4  6066  nnmsucr  6289  nnmcan  6318  xpmapenlem  6645  fundmfibi  6728  sup3exmid  8515  nzadd  8900  peano5uzti  8953  fnn0ind  8961  uztrn2  9135  irradd  9230  xltnegi  9401  xaddnemnf  9423  xaddnepnf  9424  xaddcom  9427  xnegdi  9434  elioore  9478  uzsubsubfz1  9611  fzo1fzo0n0  9743  elfzonelfzo  9790  qbtwnxr  9818  faclbnd  10280  faclbnd3  10282  dvdsprime  11547  restuni  12040  stoig  12041  cnnei  12099  tgioo  12336  bj-indind  12551