Theorem syl32anc 1258

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 1253	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:  ioom  10425  modifeq2int  10553  modaddmodup  10554  seq3f1olemqsum  10680  seq3f1o  10684  exple1  10762  leexp2rd  10870  nn0ltexp2  10876  facubnd  10912  permnn  10938  dfabsmax  11603  expcnvre  11889  dvdsadd2b  12226  dvdsmulgcd  12421  sqgcd  12425  bezoutr  12428  cncongr2  12501  pw2dvds  12563  hashgcdlem  12635  modprm0  12652  modprmn0modprm0  12654  2idlcpblrng  14360  tgioo  15101  mpodvdsmulf1o  15537  perfectlem2  15547  lgssq  15592  lgssq2  15593  gausslemma2dlem7  15620  lgsquad2lem1  15633  lgsquad2lem2  15634