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  10475  modifeq2int  10603  modaddmodup  10604  seq3f1olemqsum  10730  seq3f1o  10734  exple1  10812  leexp2rd  10920  nn0ltexp2  10926  facubnd  10962  permnn  10988  dfabsmax  11723  expcnvre  12009  dvdsadd2b  12346  dvdsmulgcd  12541  sqgcd  12545  bezoutr  12548  cncongr2  12621  pw2dvds  12683  hashgcdlem  12755  modprm0  12772  modprmn0modprm0  12774  2idlcpblrng  14481  tgioo  15222  mpodvdsmulf1o  15658  perfectlem2  15668  lgssq  15713  lgssq2  15714  gausslemma2dlem7  15741  lgsquad2lem1  15754  lgsquad2lem2  15755