Theorem syl32anc 1286

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  ioom  10712  modifeq2int  10844  modaddmodup  10845  seq3f1olemqsum  10971  seq3f1o  10975  exple1  11053  leexp2rd  11162  nn0ltexp2  11169  facubnd  11205  permnn  11232  dfabsmax  12006  expcnvre  12295  dvdsadd2b  12632  dvdsmulgcd  12827  sqgcd  12831  bezoutr  12834  cncongr2  12907  hashgcdlem  13045  modprm0  13062  modprmn0modprm0  13064  2idlcpblrng  14969  tgioo  15780  mpodvdsmulf1o  16284  perfectlem2  16300  lgssq  16364  lgssq2  16365  gausslemma2dlem7  16392  lgsquad2lem1  16405  lgsquad2lem2  16406