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  10519  modifeq2int  10647  modaddmodup  10648  seq3f1olemqsum  10774  seq3f1o  10778  exple1  10856  leexp2rd  10964  nn0ltexp2  10970  facubnd  11006  permnn  11032  dfabsmax  11777  expcnvre  12063  dvdsadd2b  12400  dvdsmulgcd  12595  sqgcd  12599  bezoutr  12602  cncongr2  12675  pw2dvds  12737  hashgcdlem  12809  modprm0  12826  modprmn0modprm0  12828  2idlcpblrng  14536  tgioo  15277  mpodvdsmulf1o  15713  perfectlem2  15723  lgssq  15768  lgssq2  15769  gausslemma2dlem7  15796  lgsquad2lem1  15809  lgsquad2lem2  15810