Theorem syl222anc 1235

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 1230	1 |- ( ph -> si )

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:  3anandis  1321  3anandirs  1322  omopth2  7136  omeu  7137  dfac12lem2  8427  xaddass2  11327  xpncan  11328  divdenle  13948  pockthlem  14087  znidomb  18122  ang180lem5  22345  isosctrlem3  22354  log2tlbnd  22476  axcontlem8  23389  xlt2addrd  26222  xrge0addass  26316  xrge0npcan  26322  congmul  29478  jm2.25lem1  29515  jm2.26  29519  jm2.27a  29522  stoweidlem42  30005  4atexlemntlpq  34070  4atexlemnclw  34072  trlval2  34165  cdleme0moN  34227  cdleme16b  34281  cdleme16c  34282  cdleme16d  34283  cdleme16e  34284  cdleme17c  34290  cdlemeda  34300  cdleme20h  34318  cdleme20j  34320  cdleme20l2  34323  cdleme21c  34329  cdleme21ct  34331  cdleme22aa  34341  cdleme22cN  34344  cdleme22d  34345  cdleme22e  34346  cdleme22eALTN  34347  cdleme23b  34352  cdleme25a  34355  cdleme25dN  34358  cdleme27N  34371  cdleme28a  34372  cdleme28b  34373  cdleme29ex  34376  cdleme32c  34445  cdleme42k  34486  cdlemg2cex  34593  cdlemg2idN  34598  cdlemg31c  34701  cdlemk5a  34837  cdlemk5  34838