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  9154  divcanap5d  9155  divcanap7d  9157  divdivap1d  9160  divdivap2d  9161  seq3coll  11315  cau3lem  11902  summodclem2a  12172  prodmodclem2a  12367  prmind2  12922  divnumden  13000  pceulem  13101  pcqmul  13110  pcqdiv  13114  pcexp  13116  pcaddlem  13146  pcbc  13158  abladdsub4  14207  ablpnpcan  14213  gsummptfidmadd  14250  lmodvs1  14761  blss2ps  15649  blss2  15650  blssps  15670  blss  15671  xmeter  15679  lgsdi  16378