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-1 5  ax-2 6  ax-3 7  ax-mp 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  6269  nchoicelem19  6305  frecexg  6310  dmfrec  6314  fnfreclem1  6315  fnfreclem2  6316  fnfreclem3  6317  frec0  6319  frecsuc  6320