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  10695  modifeq2int  10823  modaddmodup  10824  seq3f1olemqsum  10950  seq3f1o  10954  exple1  11032  leexp2rd  11141  nn0ltexp2  11147  facubnd  11183  permnn  11210  dfabsmax  11983  expcnvre  12270  dvdsadd2b  12607  dvdsmulgcd  12802  sqgcd  12806  bezoutr  12809  cncongr2  12882  pw2dvds  12944  hashgcdlem  13016  modprm0  13033  modprmn0modprm0  13035  2idlcpblrng  14860  tgioo  15655  mpodvdsmulf1o  16104  perfectlem2  16114  lgssq  16159  lgssq2  16160  gausslemma2dlem7  16187  lgsquad2lem1  16200  lgsquad2lem2  16201