Theorem syl222anc 1244

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 )
sylXanc.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		sylXanc.1	. 2 |- ( ph -> ps )
2		sylXanc.2	. 2 |- ( ph -> ch )
3		sylXanc.3	. 2 |- ( ph -> th )
4		sylXanc.4	. 2 |- ( ph -> ta )
5		sylXanc.5	. . 3 |- ( ph -> et )
6		sylXanc.6	. . 3 |- ( ph -> ze )
7	5, 6	jca 532	. 2 |- ( ph -> ( et /\ ze ) )
8		syl222anc.7	. 2 |- ( ( ( ps /\ ch ) /\ ( th /\ ta ) /\ ( et /\ ze ) ) -> si )
9	1, 2, 3, 4, 7, 8	syl221anc 1239	1 |- ( ph -> si )

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:  3anandis  1330  3anandirs  1331  omopth2  7234  omeu  7235  dfac12lem2  8525  xaddass2  11443  xpncan  11444  divdenle  14144  pockthlem  14285  znidomb  18407  ang180lem5  22970  isosctrlem3  22979  log2tlbnd  23101  axcontlem8  24047  xlt2addrd  27343  xrge0addass  27437  xrge0npcan  27443  congmul  30736  jm2.25lem1  30771  jm2.26  30775  jm2.27a  30778  stoweidlem42  31569  4atexlemntlpq  35081  4atexlemnclw  35083  trlval2  35176  cdleme0moN  35238  cdleme16b  35292  cdleme16c  35293  cdleme16d  35294  cdleme16e  35295  cdleme17c  35301  cdlemeda  35311  cdleme20h  35329  cdleme20j  35331  cdleme20l2  35334  cdleme21c  35340  cdleme21ct  35342  cdleme22aa  35352  cdleme22cN  35355  cdleme22d  35356  cdleme22e  35357  cdleme22eALTN  35358  cdleme23b  35363  cdleme25a  35366  cdleme25dN  35369  cdleme27N  35382  cdleme28a  35383  cdleme28b  35384  cdleme29ex  35387  cdleme32c  35456  cdleme42k  35497  cdlemg2cex  35604  cdlemg2idN  35609  cdlemg31c  35712  cdlemk5a  35848  cdlemk5  35849