Theorem syl32anc 1282

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

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

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 1007

This theorem is referenced by:  ioom  10620  modifeq2int  10748  modaddmodup  10749  seq3f1olemqsum  10875  seq3f1o  10879  exple1  10957  leexp2rd  11065  nn0ltexp2  11071  facubnd  11107  permnn  11134  dfabsmax  11902  expcnvre  12189  dvdsadd2b  12526  dvdsmulgcd  12721  sqgcd  12725  bezoutr  12728  cncongr2  12801  pw2dvds  12863  hashgcdlem  12935  modprm0  12952  modprmn0modprm0  12954  2idlcpblrng  14671  tgioo  15419  mpodvdsmulf1o  15858  perfectlem2  15868  lgssq  15913  lgssq2  15914  gausslemma2dlem7  15941  lgsquad2lem1  15954  lgsquad2lem2  15955