Theorem sylancr 644

Description: Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.)

Hypotheses

Ref	Expression
sylancr.1	|- ps
sylancr.2	|- (ph -> ch)
sylancr.3	|- ((ps /\ ch) -> th)

Assertion

Ref	Expression
sylancr	|- (ph -> th)

Proof of Theorem sylancr

Step	Hyp	Ref	Expression
1		sylancr.1	. . 3 |- ps
2	1	a1i 10	. 2 |- (ph -> ps)
3		sylancr.2	. 2 |- (ph -> ch)
4		sylancr.3	. 2 |- ((ps /\ ch) -> th)
5	2, 3, 4	syl2anc 642	1 |- (ph -> th)

Syntax hints:   -> wi 4   /\ wa 358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  unipw  4118  imakexg  4300  pwexg  4329  snfi  4432  1cspfin  4544  vfintle  4547  vfin1cltv  4548  phialllem2  4618  coexg  4750  ov  5596  mpteq2da  5667  brcupg  5815  brcomposeg  5820  brcrossg  5849  frds  5936  qsexg  5983  enmap2lem5  6068  enmap1lem5  6074  enprmaplem6  6082  enpw  6088  dflec2  6211  nmembers1lem3  6271  nchoicelem19  6308  frecexg  6313  dmfrec  6317  fnfreclem1  6318  fnfreclem2  6319  fnfreclem3  6320  frec0  6322  frecsuc  6323