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  2484  rmob  3125  disjne  3548  seex  4432  tron  4479  fssres  5512  funbrfvb  5686  funopfvb  5687  fvelrnb  5693  fvco  5716  fvimacnvi  5761  ffvresb  5810  fcof  5832  funresdfunsnss  5856  fvtp2g  5862  fvtp2  5865  fnex  5875  funex  5876  1st2nd  6343  dftpos4  6428  nnmsucr  6655  nnmcan  6686  xpmapenlem  7034  fundmfibi  7136  sup3exmid  9136  nzadd  9531  peano5uzti  9587  fnn0ind  9595  uztrn2  9773  irradd  9879  xltnegi  10069  xaddnemnf  10091  xaddnepnf  10092  xaddcom  10095  xnegdi  10102  elioore  10146  uzsubsubfz1  10282  fzo1fzo0n0  10421  elfzonelfzo  10474  qbtwnxr  10516  faclbnd  11002  faclbnd3  11004  swrdccat3b  11320  dvdsprime  12693  pcgcd  12901  znf1o  14664  restuni  14895  stoig  14896  cnnei  14955  tgioo  15277  divcnap  15288  ivthdich  15376  lgsdi  15765  bj-indind  16527