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 )

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

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 1011

This theorem is referenced by:  ioom  10676  modifeq2int  10804  modaddmodup  10805  seq3f1olemqsum  10931  seq3f1o  10935  exple1  11013  leexp2rd  11122  nn0ltexp2  11128  facubnd  11164  permnn  11191  dfabsmax  11964  expcnvre  12251  dvdsadd2b  12588  dvdsmulgcd  12783  sqgcd  12787  bezoutr  12790  cncongr2  12863  pw2dvds  12925  hashgcdlem  12997  modprm0  13014  modprmn0modprm0  13016  2idlcpblrng  14835  tgioo  15581  mpodvdsmulf1o  16021  perfectlem2  16031  lgssq  16076  lgssq2  16077  gausslemma2dlem7  16104  lgsquad2lem1  16117  lgsquad2lem2  16118