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  10401  modifeq2int  10529  modaddmodup  10530  seq3f1olemqsum  10656  seq3f1o  10660  exple1  10738  leexp2rd  10846  nn0ltexp2  10852  facubnd  10888  permnn  10914  dfabsmax  11470  expcnvre  11756  dvdsadd2b  12093  dvdsmulgcd  12288  sqgcd  12292  bezoutr  12295  cncongr2  12368  pw2dvds  12430  hashgcdlem  12502  modprm0  12519  modprmn0modprm0  12521  2idlcpblrng  14227  tgioo  14968  mpodvdsmulf1o  15404  perfectlem2  15414  lgssq  15459  lgssq2  15460  gausslemma2dlem7  15487  lgsquad2lem1  15500  lgsquad2lem2  15501