Theorem syl32anc 1282

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

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

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 1007

This theorem is referenced by:  ioom  10644  modifeq2int  10772  modaddmodup  10773  seq3f1olemqsum  10899  seq3f1o  10903  exple1  10981  leexp2rd  11090  nn0ltexp2  11096  facubnd  11132  permnn  11159  dfabsmax  11927  expcnvre  12214  dvdsadd2b  12551  dvdsmulgcd  12746  sqgcd  12750  bezoutr  12753  cncongr2  12826  pw2dvds  12888  hashgcdlem  12960  modprm0  12977  modprmn0modprm0  12979  2idlcpblrng  14797  tgioo  15545  mpodvdsmulf1o  15984  perfectlem2  15994  lgssq  16039  lgssq2  16040  gausslemma2dlem7  16067  lgsquad2lem1  16080  lgsquad2lem2  16081