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  10566  modifeq2int  10694  modaddmodup  10695  seq3f1olemqsum  10821  seq3f1o  10825  exple1  10903  leexp2rd  11011  nn0ltexp2  11017  facubnd  11053  permnn  11079  dfabsmax  11840  expcnvre  12127  dvdsadd2b  12464  dvdsmulgcd  12659  sqgcd  12663  bezoutr  12666  cncongr2  12739  pw2dvds  12801  hashgcdlem  12873  modprm0  12890  modprmn0modprm0  12892  2idlcpblrng  14602  tgioo  15348  mpodvdsmulf1o  15787  perfectlem2  15797  lgssq  15842  lgssq2  15843  gausslemma2dlem7  15870  lgsquad2lem1  15883  lgsquad2lem2  15884