Theorem syl32anc 1257

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

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

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 982

This theorem is referenced by:  ioom  10350  modifeq2int  10478  modaddmodup  10479  seq3f1olemqsum  10605  seq3f1o  10609  exple1  10687  leexp2rd  10795  nn0ltexp2  10801  facubnd  10837  permnn  10863  dfabsmax  11382  expcnvre  11668  dvdsadd2b  12005  dvdsmulgcd  12192  sqgcd  12196  bezoutr  12199  cncongr2  12272  pw2dvds  12334  hashgcdlem  12406  modprm0  12423  modprmn0modprm0  12425  2idlcpblrng  14079  tgioo  14790  mpodvdsmulf1o  15226  perfectlem2  15236  lgssq  15281  lgssq2  15282  gausslemma2dlem7  15309  lgsquad2lem1  15322  lgsquad2lem2  15323