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  2170  eqtr2  2248  pm13.181  2482  rmob  3122  disjne  3545  seex  4427  tron  4474  fssres  5506  funbrfvb  5679  funopfvb  5680  fvelrnb  5686  fvco  5709  fvimacnvi  5754  ffvresb  5803  fcof  5825  funresdfunsnss  5849  fvtp2g  5855  fvtp2  5858  fnex  5868  funex  5869  1st2nd  6336  dftpos4  6420  nnmsucr  6647  nnmcan  6678  xpmapenlem  7023  fundmfibi  7121  sup3exmid  9120  nzadd  9515  peano5uzti  9571  fnn0ind  9579  uztrn2  9757  irradd  9858  xltnegi  10048  xaddnemnf  10070  xaddnepnf  10071  xaddcom  10074  xnegdi  10081  elioore  10125  uzsubsubfz1  10261  fzo1fzo0n0  10400  elfzonelfzo  10453  qbtwnxr  10494  faclbnd  10980  faclbnd3  10982  swrdccat3b  11293  dvdsprime  12665  pcgcd  12873  znf1o  14636  restuni  14867  stoig  14868  cnnei  14927  tgioo  15249  divcnap  15260  ivthdich  15348  lgsdi  15737  bj-indind  16404