Theorem syl221anc 1229

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 1224	1 |- ( ph -> ze )

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

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 967

This theorem is referenced by:  syl222anc  1234  vtocldf  3021  f1oprswap  5680  dmdcand  10136  modmul12d  11753  modnegd  11754  modadd12d  11755  exprec  11905  splval2  12399  eulerthlem2  13857  fermltl  13859  odzdvds  13867  efgredleme  16240  efgredlemc  16242  blssps  19999  blss  20000  metequiv2  20085  met1stc  20096  met2ndci  20097  metdstri  20427  xlebnum  20537  caubl  20818  divcxp  22132  cxple2a  22144  cxplead  22166  cxplt2d  22171  cxple2d  22172  mulcxpd  22173  ang180  22210  wilthlem2  22407  lgslem4  22638  lgsvalmod  22654  lgsmod  22660  lgsdir2lem4  22665  lgsdirprm  22668  lgsne0  22672  lgseisen  22692  ax5seglem9  23183  xrsmulgzz  26139  heiborlem8  28717  pellexlem6  29175  rpexpmord  29289  acongeq  29326  jm2.25  29348  stoweidlem42  29837  stoweidlem51  29846  ldepspr  31007  cdlemd4  33845  cdleme15a  33918  cdleme17b  33931  cdleme25a  33997  cdleme25c  33999  cdleme25dN  34000  cdleme26ee  34004  tendococl  34416  tendodi1  34428  tendodi2  34429  cdlemi  34464  tendocan  34468  cdlemk5a  34479  cdlemk5  34480  cdlemk10  34487  cdlemk5u  34505  cdlemkfid1N  34565