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 )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 1009

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 1011

This theorem is referenced by:  ioom  10673  modifeq2int  10801  modaddmodup  10802  seq3f1olemqsum  10928  seq3f1o  10932  exple1  11010  leexp2rd  11119  nn0ltexp2  11125  facubnd  11161  permnn  11188  dfabsmax  11961  expcnvre  12248  dvdsadd2b  12585  dvdsmulgcd  12780  sqgcd  12784  bezoutr  12787  cncongr2  12860  pw2dvds  12922  hashgcdlem  12994  modprm0  13011  modprmn0modprm0  13013  2idlcpblrng  14832  tgioo  15578  mpodvdsmulf1o  16018  perfectlem2  16028  lgssq  16073  lgssq2  16074  gausslemma2dlem7  16101  lgsquad2lem1  16114  lgsquad2lem2  16115