Theorem syl211anc 1332

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
syl12anc.1	|- ( ph -> ps )
syl12anc.2	|- ( ph -> ch )
syl12anc.3	|- ( ph -> th )
syl22anc.4	|- ( ph -> ta )
syl211anc.5	|- ( ( ( ps /\ ch ) /\ th /\ ta ) -> et )

Assertion

Ref	Expression
syl211anc	|- ( ph -> et )

Proof of Theorem syl211anc

Step	Hyp	Ref	Expression
1		syl12anc.1	. . 3 |- ( ph -> ps )
2		syl12anc.2	. . 3 |- ( ph -> ch )
3	1, 2	jca 554	. 2 |- ( ph -> ( ps /\ ch ) )
4		syl12anc.3	. 2 |- ( ph -> th )
5		syl22anc.4	. 2 |- ( ph -> ta )
6		syl211anc.5	. 2 |- ( ( ( ps /\ ch ) /\ th /\ ta ) -> et )
7	3, 4, 5, 6	syl3anc 1326	1 |- ( ph -> et )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039

This theorem is referenced by:  syl212anc  1336  syl221anc  1337  supicc  12320  modaddmulmod  12737  limsupgre  14212  limsupbnd1  14213  limsupbnd2  14214  lbspss  19082  lindff1  20159  islinds4  20174  mdetunilem9  20426  madutpos  20448  neiptopnei  20936  mbflimsup  23433  cxpneg  24427  cxpmul2  24435  cxpsqrt  24449  cxpaddd  24463  cxpsubd  24464  divcxpd  24468  fsumharmonic  24738  bposlem1  25009  lgsqr  25076  chpchtlim  25168  ax5seg  25818  archiabllem2c  29749  logdivsqrle  30728  lshpnelb  34271  cdlemg2fv2  35888  cdlemg2m  35892  cdlemg9a  35920  cdlemg9b  35921  cdlemg12b  35932  cdlemg14f  35941  cdlemg14g  35942  cdlemg17dN  35951  cdlemkj  36151  cdlemkuv2  36155  cdlemk52  36242  cdlemk53a  36243  mullimc  39848  mullimcf  39855  sfprmdvdsmersenne  41520  lincfsuppcl  42202