Theorem syl32anc 1279

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 )
syl32anc.6	|- ( ( ( ps /\ ch /\ th ) /\ ( ta /\ et ) ) -> ze )

Assertion

Ref	Expression
syl32anc	|- ( ph -> ze )

Proof of Theorem syl32anc

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		syl32anc.6	. 2 |- ( ( ( ps /\ ch /\ th ) /\ ( ta /\ et ) ) -> ze )
8	1, 2, 3, 6, 7	syl31anc 1274	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:  ioom  10510  modifeq2int  10638  modaddmodup  10639  seq3f1olemqsum  10765  seq3f1o  10769  exple1  10847  leexp2rd  10955  nn0ltexp2  10961  facubnd  10997  permnn  11023  dfabsmax  11768  expcnvre  12054  dvdsadd2b  12391  dvdsmulgcd  12586  sqgcd  12590  bezoutr  12593  cncongr2  12666  pw2dvds  12728  hashgcdlem  12800  modprm0  12817  modprmn0modprm0  12819  2idlcpblrng  14527  tgioo  15268  mpodvdsmulf1o  15704  perfectlem2  15714  lgssq  15759  lgssq2  15760  gausslemma2dlem7  15787  lgsquad2lem1  15800  lgsquad2lem2  15801