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  10705  modifeq2int  10836  modaddmodup  10837  seq3f1olemqsum  10963  seq3f1o  10967  exple1  11045  leexp2rd  11154  nn0ltexp2  11161  facubnd  11197  permnn  11224  dfabsmax  11998  expcnvre  12286  dvdsadd2b  12623  dvdsmulgcd  12818  sqgcd  12822  bezoutr  12825  cncongr2  12898  hashgcdlem  13036  modprm0  13053  modprmn0modprm0  13055  2idlcpblrng  14909  tgioo  15704  mpodvdsmulf1o  16185  perfectlem2  16198  lgssq  16257  lgssq2  16258  gausslemma2dlem7  16285  lgsquad2lem1  16298  lgsquad2lem2  16299