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  4117  imakexg  4299  pwexg  4328  snfi  4431  1cspfin  4543  vfintle  4546  vfin1cltv  4547  phialllem2  4617  coexg  4749  ov  5595  mpteq2da  5666  brcupg  5814  brcomposeg  5819  brcrossg  5848  frds  5935  qsexg  5982  enmap2lem5  6067  enmap1lem5  6073  enprmaplem6  6081  enpw  6087  dflec2  6210  nmembers1lem3  6270  nchoicelem19  6307  frecexg  6312  dmfrec  6316  fnfreclem1  6317  fnfreclem2  6318  fnfreclem3  6319  frec0  6321  frecsuc  6322