Theorem syl23anc 1333

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 )
syl23anc.5	|- ( ph -> et )
syl23anc.6	|- ( ( ( ps /\ ch ) /\ ( th /\ ta /\ et ) ) -> ze )

Assertion

Ref	Expression
syl23anc	|- ( ph -> ze )

Proof of Theorem syl23anc

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		syl23anc.5	. 2 |- ( ph -> et )
7		syl23anc.6	. 2 |- ( ( ( ps /\ ch ) /\ ( th /\ ta /\ et ) ) -> ze )
8	3, 4, 5, 6, 7	syl13anc 1328	1 |- ( ph -> ze )

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:  suppofss1d  7332  suppofss2d  7333  cnfcomlem  8596  ackbij1lem16  9057  div2subd  10851  symg2bas  17818  evl1expd  19709  psgndiflemA  19947  oftpos  20258  restopn2  20981  tsmsxp  21958  blcld  22310  metustexhalf  22361  cnllycmp  22755  dvlipcn  23757  tanregt0  24285  ostthlem1  25316  ax5seglem6  25814  axcontlem4  25847  axcontlem7  25850  wwlksnextwrd  26792  pnfneige0  29997  qqhval2  30026  esumcocn  30142  carsgmon  30376  bnj1125  31060  nosupbnd1lem1  31854  nosupbnd2  31862  heiborlem8  33617  2atjm  34731  1cvrat  34762  lvolnlelln  34870  lvolnlelpln  34871  4atlem3  34882  lplncvrlvol  34902  dalem39  34997  cdleme4a  35526  cdleme15  35565  cdleme16c  35567  cdleme19b  35592  cdleme19e  35595  cdleme20d  35600  cdleme20g  35603  cdleme20j  35606  cdleme20k  35607  cdleme20l2  35609  cdleme20l  35610  cdleme20m  35611  cdleme22e  35632  cdleme22eALTN  35633  cdleme22f  35634  cdleme27cl  35654  cdlemefr27cl  35691  mpaaeu  37720