Theorem syl221anc 1239

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
sylXanc.1	|- ( ph -> ps )
sylXanc.2	|- ( ph -> ch )
sylXanc.3	|- ( ph -> th )
sylXanc.4	|- ( ph -> ta )
sylXanc.5	|- ( ph -> et )
syl221anc.6	|- ( ( ( ps /\ ch ) /\ ( th /\ ta ) /\ et ) -> ze )

Assertion

Ref	Expression
syl221anc	|- ( ph -> ze )

Proof of Theorem syl221anc

Step	Hyp	Ref	Expression
1		sylXanc.1	. 2 |- ( ph -> ps )
2		sylXanc.2	. 2 |- ( ph -> ch )
3		sylXanc.3	. . 3 |- ( ph -> th )
4		sylXanc.4	. . 3 |- ( ph -> ta )
5	3, 4	jca 532	. 2 |- ( ph -> ( th /\ ta ) )
6		sylXanc.5	. 2 |- ( ph -> et )
7		syl221anc.6	. 2 |- ( ( ( ps /\ ch ) /\ ( th /\ ta ) /\ et ) -> ze )
8	1, 2, 5, 6, 7	syl211anc 1234	1 |- ( ph -> ze )

Syntax hints:   -> wi 4   /\ wa 369   /\ w3a 973

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 185  df-an 371  df-3an 975

This theorem is referenced by:  syl222anc  1244  vtocldf  3162  f1oprswap  5853  dmdcand  10345  modmul12d  12004  modnegd  12005  modadd12d  12006  exprec  12169  splval2  12690  eulerthlem2  14164  fermltl  14166  odzdvds  14174  efgredleme  16554  efgredlemc  16556  blssps  20659  blss  20660  metequiv2  20745  met1stc  20756  met2ndci  20757  metdstri  21087  xlebnum  21197  caubl  21478  divcxp  22793  cxple2a  22805  cxplead  22827  cxplt2d  22832  cxple2d  22833  mulcxpd  22834  ang180  22871  wilthlem2  23068  lgslem4  23299  lgsvalmod  23315  lgsmod  23321  lgsdir2lem4  23326  lgsdirprm  23329  lgsne0  23333  lgseisen  23353  ax5seglem9  23913  xrsmulgzz  27325  heiborlem8  29915  pellexlem6  30372  rpexpmord  30486  acongeq  30523  jm2.25  30545  stoweidlem42  31342  stoweidlem51  31351  ldepspr  32147  cdlemd4  34997  cdleme15a  35070  cdleme17b  35083  cdleme25a  35149  cdleme25c  35151  cdleme25dN  35152  cdleme26ee  35156  tendococl  35568  tendodi1  35580  tendodi2  35581  cdlemi  35616  tendocan  35620  cdlemk5a  35631  cdlemk5  35632  cdlemk10  35639  cdlemk5u  35657  cdlemkfid1N  35717