Theorem syl122anc 1259

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

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

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 983

This theorem is referenced by:  divdiv32apd  8889  divcanap5d  8890  divcanap7d  8892  divdivap1d  8895  divdivap2d  8896  seq3coll  10987  cau3lem  11425  summodclem2a  11692  prodmodclem2a  11887  prmind2  12442  divnumden  12518  pceulem  12617  pcqmul  12626  pcqdiv  12630  pcexp  12632  pcaddlem  12662  pcbc  12674  abladdsub4  13650  ablpnpcan  13656  lmodvs1  14078  blss2ps  14878  blss2  14879  blssps  14899  blss  14900  xmeter  14908  lgsdi  15514