Theorem syl122anc 1280

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 1276	1 |- ( ph -> ze )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 1002

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1004

This theorem is referenced by:  divdiv32apd  8959  divcanap5d  8960  divcanap7d  8962  divdivap1d  8965  divdivap2d  8966  seq3coll  11059  cau3lem  11620  summodclem2a  11887  prodmodclem2a  12082  prmind2  12637  divnumden  12713  pceulem  12812  pcqmul  12821  pcqdiv  12825  pcexp  12827  pcaddlem  12857  pcbc  12869  abladdsub4  13846  ablpnpcan  13852  lmodvs1  14274  blss2ps  15074  blss2  15075  blssps  15095  blss  15096  xmeter  15104  lgsdi  15710