Theorem syl221anc 1303

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

Hypotheses

Ref	Expression
syl12anc.1	|- ( ph -> ps )
syl12anc.2	|- ( ph -> ch )
syl12anc.3	|- ( ph -> th )
syl22anc.4	|- ( ph -> ta )
syl23anc.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		syl12anc.1	. 2 |- ( ph -> ps )
2		syl12anc.2	. 2 |- ( ph -> ch )
3		syl12anc.3	. . 3 |- ( ph -> th )
4		syl22anc.4	. . 3 |- ( ph -> ta )
5	3, 4	jca 541	. 2 |- ( ph -> ( th /\ ta ) )
6		syl23anc.5	. 2 |- ( ph -> et )
7		syl221anc.6	. 2 |- ( ( ( ps /\ ch ) /\ ( th /\ ta ) /\ et ) -> ze )
8	1, 2, 5, 6, 7	syl211anc 1298	1 |- ( ph -> ze )

Syntax hints:   -> wi 4   /\ wa 376   /\ w3a 1007

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 190  df-an 378  df-3an 1009

This theorem is referenced by:  syl222anc  1308  vtocldf  3083  f1oprswap  5868  dmdcand  10434  modmul12d  12178  modnegd  12179  modadd12d  12180  exprec  12351  splval2  12918  eulerthlem2  14809  fermltl  14811  odzdvds  14819  odzdvdsOLD  14825  efgredleme  17471  efgredlemc  17473  blssps  21517  blss  21518  metequiv2  21603  met1stc  21614  met2ndci  21615  metdstri  21946  metdstriOLD  21961  xlebnum  22074  caubl  22355  divcxp  23711  cxple2a  23723  cxplead  23745  cxplt2d  23750  cxple2d  23751  mulcxpd  23752  ang180  23822  wilthlem2  24073  lgslem4  24306  lgsvalmod  24322  lgsmod  24328  lgsdir2lem4  24333  lgsdirprm  24336  lgsne0  24340  lgseisen  24360  ax5seglem9  25046  xrsmulgzz  28515  heiborlem8  32214  cdlemd4  33838  cdleme15a  33911  cdleme17b  33924  cdleme25a  33991  cdleme25c  33993  cdleme25dN  33994  cdleme26ee  33998  tendococl  34410  tendodi1  34422  tendodi2  34423  cdlemi  34458  tendocan  34462  cdlemk5a  34473  cdlemk5  34474  cdlemk10  34481  cdlemk5u  34499  cdlemkfid1N  34559  pellexlem6  35749  rpexpmord  35867  acongeq  35904  jm2.25  35925  stoweidlem42  38015  stoweidlem51  38024  ldepspr  40774