Theorem syl222anc 1342

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 )
syl33anc.6	|- ( ph -> ze )
syl222anc.7	|- ( ( ( ps /\ ch ) /\ ( th /\ ta ) /\ ( et /\ ze ) ) -> si )

Assertion

Ref	Expression
syl222anc	|- ( ph -> si )

Proof of Theorem syl222anc

Step	Hyp	Ref	Expression
1		syl12anc.1	. 2 |- ( ph -> ps )
2		syl12anc.2	. 2 |- ( ph -> ch )
3		syl12anc.3	. 2 |- ( ph -> th )
4		syl22anc.4	. 2 |- ( ph -> ta )
5		syl23anc.5	. . 3 |- ( ph -> et )
6		syl33anc.6	. . 3 |- ( ph -> ze )
7	5, 6	jca 554	. 2 |- ( ph -> ( et /\ ze ) )
8		syl222anc.7	. 2 |- ( ( ( ps /\ ch ) /\ ( th /\ ta ) /\ ( et /\ ze ) ) -> si )
9	1, 2, 3, 4, 7, 8	syl221anc 1337	1 |- ( ph -> si )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  3anandis  1434  3anandirs  1435  omopth2  7664  omeu  7665  dfac12lem2  8966  xaddass2  12080  xpncan  12081  divdenle  15457  pockthlem  15609  znidomb  19910  tanord1  24283  ang180lem5  24543  isosctrlem3  24550  log2tlbnd  24672  basellem1  24807  perfectlem2  24955  bposlem6  25014  dchrisum0flblem2  25198  pntpbnd1a  25274  axcontlem8  25851  xlt2addrd  29523  xrge0addass  29690  xrge0npcan  29694  submatminr1  29876  carsgclctunlem2  30381  4atexlemntlpq  35354  4atexlemnclw  35356  trlval2  35450  cdleme0moN  35512  cdleme16b  35566  cdleme16c  35567  cdleme16d  35568  cdleme16e  35569  cdleme17c  35575  cdlemeda  35585  cdleme20h  35604  cdleme20j  35606  cdleme20l2  35609  cdleme21c  35615  cdleme21ct  35617  cdleme22aa  35627  cdleme22cN  35630  cdleme22d  35631  cdleme22e  35632  cdleme22eALTN  35633  cdleme23b  35638  cdleme25a  35641  cdleme25dN  35644  cdleme27N  35657  cdleme28a  35658  cdleme28b  35659  cdleme29ex  35662  cdleme32c  35731  cdleme42k  35772  cdlemg2cex  35879  cdlemg2idN  35884  cdlemg31c  35987  cdlemk5a  36123  cdlemk5  36124  congmul  37534  jm2.25lem1  37565  jm2.26  37569  jm2.27a  37572  infleinflem1  39586  stoweidlem42  40259