Theorem syl122anc 1287

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

Assertion

Ref	Expression
syl122anc	|- ( ph -> ze )

Proof of Theorem syl122anc

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	. . 3 |- ( ph -> ta )
5		sylXanc.5	. . 3 |- ( ph -> et )
6	4, 5	jca 306	. 2 |- ( ph -> ( ta /\ et ) )
7		syl122anc.6	. 2 |- ( ( ps /\ ( ch /\ th ) /\ ( ta /\ et ) ) -> ze )
8	1, 2, 3, 6, 7	syl121anc 1283	1 |- ( ph -> ze )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  divdiv32apd  9148  divcanap5d  9149  divcanap7d  9151  divdivap1d  9154  divdivap2d  9155  seq3coll  11308  cau3lem  11895  summodclem2a  12164  prodmodclem2a  12359  prmind2  12914  divnumden  12992  pceulem  13093  pcqmul  13102  pcqdiv  13106  pcexp  13108  pcaddlem  13138  pcbc  13150  abladdsub4  14167  ablpnpcan  14173  gsummptfidmadd  14210  lmodvs1  14702  blss2ps  15556  blss2  15557  blssps  15577  blss  15578  xmeter  15586  lgsdi  16254