Theorem syl122anc 1247

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

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

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 980

This theorem is referenced by:  divdiv32apd  8759  divcanap5d  8760  divcanap7d  8762  divdivap1d  8765  divdivap2d  8766  seq3coll  10803  cau3lem  11104  summodclem2a  11370  prodmodclem2a  11565  prmind2  12100  divnumden  12176  pceulem  12274  pcqmul  12283  pcqdiv  12287  pcexp  12289  pcaddlem  12318  pcbc  12329  abladdsub4  12941  ablpnpcan  12947  blss2ps  13566  blss2  13567  blssps  13587  blss  13588  xmeter  13596  lgsdi  14098