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  10384  modifeq2int  10512  modaddmodup  10513  seq3f1olemqsum  10639  seq3f1o  10643  exple1  10721  leexp2rd  10829  nn0ltexp2  10835  facubnd  10871  permnn  10897  dfabsmax  11447  expcnvre  11733  dvdsadd2b  12070  dvdsmulgcd  12265  sqgcd  12269  bezoutr  12272  cncongr2  12345  pw2dvds  12407  hashgcdlem  12479  modprm0  12496  modprmn0modprm0  12498  2idlcpblrng  14203  tgioo  14944  mpodvdsmulf1o  15380  perfectlem2  15390  lgssq  15435  lgssq2  15436  gausslemma2dlem7  15463  lgsquad2lem1  15476  lgsquad2lem2  15477