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  5833  funresdfunsnss  5857  fvtp2g  5863  fvtp2  5866  fnex  5876  funex  5877  1st2nd  6344  dftpos4  6429  nnmsucr  6656  nnmcan  6687  xpmapenlem  7035  fundmfibi  7137  sup3exmid  9137  nzadd  9532  peano5uzti  9588  fnn0ind  9596  uztrn2  9774  irradd  9880  xltnegi  10070  xaddnemnf  10092  xaddnepnf  10093  xaddcom  10096  xnegdi  10103  elioore  10147  uzsubsubfz1  10283  fzo1fzo0n0  10423  elfzonelfzo  10476  qbtwnxr  10518  faclbnd  11004  faclbnd3  11006  swrdccat3b  11325  dvdsprime  12699  pcgcd  12907  znf1o  14671  restuni  14902  stoig  14903  cnnei  14962  tgioo  15284  divcnap  15295  ivthdich  15383  lgsdi  15772  bj-indind  16553