Theorem syl122anc 1236

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 304	. 2 |- ( ph -> ( ta /\ et ) )
7		syl122anc.6	. 2 |- ( ( ps /\ ( ch /\ th ) /\ ( ta /\ et ) ) -> ze )
8	1, 2, 3, 6, 7	syl121anc 1232	1 |- ( ph -> ze )

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 967

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

This theorem depends on definitions:  df-bi 116  df-3an 969

This theorem is referenced by:  divdiv32apd  8703  divcanap5d  8704  divcanap7d  8706  divdivap1d  8709  divdivap2d  8710  seq3coll  10741  cau3lem  11042  summodclem2a  11308  prodmodclem2a  11503  prmind2  12031  divnumden  12105  pceulem  12203  pcqmul  12212  pcqdiv  12216  pcexp  12218  pcaddlem  12247  pcbc  12258  blss2ps  12947  blss2  12948  blssps  12968  blss  12969  xmeter  12977