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  10706  modifeq2int  10838  modaddmodup  10839  seq3f1olemqsum  10965  seq3f1o  10969  exple1  11047  leexp2rd  11156  nn0ltexp2  11163  facubnd  11199  permnn  11226  dfabsmax  12000  expcnvre  12289  dvdsadd2b  12626  dvdsmulgcd  12821  sqgcd  12825  bezoutr  12828  cncongr2  12901  hashgcdlem  13039  modprm0  13056  modprmn0modprm0  13058  2idlcpblrng  14944  tgioo  15746  mpodvdsmulf1o  16245  perfectlem2  16261  lgssq  16325  lgssq2  16326  gausslemma2dlem7  16353  lgsquad2lem1  16366  lgsquad2lem2  16367