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  10492  modifeq2int  10620  modaddmodup  10621  seq3f1olemqsum  10747  seq3f1o  10751  exple1  10829  leexp2rd  10937  nn0ltexp2  10943  facubnd  10979  permnn  11005  dfabsmax  11743  expcnvre  12029  dvdsadd2b  12366  dvdsmulgcd  12561  sqgcd  12565  bezoutr  12568  cncongr2  12641  pw2dvds  12703  hashgcdlem  12775  modprm0  12792  modprmn0modprm0  12794  2idlcpblrng  14502  tgioo  15243  mpodvdsmulf1o  15679  perfectlem2  15689  lgssq  15734  lgssq2  15735  gausslemma2dlem7  15762  lgsquad2lem1  15775  lgsquad2lem2  15776