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  10711  modifeq2int  10843  modaddmodup  10844  seq3f1olemqsum  10970  seq3f1o  10974  exple1  11052  leexp2rd  11161  nn0ltexp2  11168  facubnd  11204  permnn  11231  dfabsmax  12005  expcnvre  12294  dvdsadd2b  12631  dvdsmulgcd  12826  sqgcd  12830  bezoutr  12833  cncongr2  12906  hashgcdlem  13044  modprm0  13061  modprmn0modprm0  13063  2idlcpblrng  14968  tgioo  15797  mpodvdsmulf1o  16301  perfectlem2  16317  lgssq  16381  lgssq2  16382  gausslemma2dlem7  16409  lgsquad2lem1  16422  lgsquad2lem2  16423