Theorem syl32anc 1281

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

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

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 1006

This theorem is referenced by:  ioom  10521  modifeq2int  10649  modaddmodup  10650  seq3f1olemqsum  10776  seq3f1o  10780  exple1  10858  leexp2rd  10966  nn0ltexp2  10972  facubnd  11008  permnn  11034  dfabsmax  11795  expcnvre  12082  dvdsadd2b  12419  dvdsmulgcd  12614  sqgcd  12618  bezoutr  12621  cncongr2  12694  pw2dvds  12756  hashgcdlem  12828  modprm0  12845  modprmn0modprm0  12847  2idlcpblrng  14556  tgioo  15297  mpodvdsmulf1o  15733  perfectlem2  15743  lgssq  15788  lgssq2  15789  gausslemma2dlem7  15816  lgsquad2lem1  15829  lgsquad2lem2  15830