Theorem syl23anc 1225

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

Assertion

Ref	Expression
syl23anc	|- ( ph -> ze )

Proof of Theorem syl23anc

Step	Hyp	Ref	Expression
1		sylXanc.1	. . 3 |- ( ph -> ps )
2		sylXanc.2	. . 3 |- ( ph -> ch )
3	1, 2	jca 532	. 2 |- ( ph -> ( ps /\ ch ) )
4		sylXanc.3	. 2 |- ( ph -> th )
5		sylXanc.4	. 2 |- ( ph -> ta )
6		sylXanc.5	. 2 |- ( ph -> et )
7		syl23anc.6	. 2 |- ( ( ( ps /\ ch ) /\ ( th /\ ta /\ et ) ) -> ze )
8	3, 4, 5, 6, 7	syl13anc 1220	1 |- ( ph -> ze )

Syntax hints:   -> wi 4   /\ wa 369   /\ w3a 965

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 185  df-an 371  df-3an 967

This theorem is referenced by:  suppofss1d  6721  suppofss2d  6722  cnfcomlem  7924  cnfcomlemOLD  7932  ackbij1lem16  8396  div2subd  10149  symg2bas  15894  evl1expd  17754  psgndiflemA  18006  oftpos  18308  restopn2  18756  tsmsxp  19704  blcld  20055  metustexhalfOLD  20113  metustexhalf  20114  cnllycmp  20503  dvlipcn  21441  tanregt0  21970  ostthlem1  22851  ax5seglem6  23131  axcontlem4  23164  axcontlem7  23167  pnfneige0  26333  qqhval2  26363  esumcocn  26481  heiborlem8  28670  mpaaeu  29460  wwlkextwrd  30313  bnj1125  31870  2atjm  32929  1cvrat  32960  lvolnlelln  33068  lvolnlelpln  33069  4atlem3  33080  lplncvrlvol  33100  dalem39  33195  cdleme4a  33723  cdleme15  33762  cdleme16c  33764  cdleme19b  33788  cdleme19e  33791  cdleme20d  33796  cdleme20g  33799  cdleme20j  33802  cdleme20k  33803  cdleme20l2  33805  cdleme20l  33806  cdleme20m  33807  cdleme22e  33828  cdleme22eALTN  33829  cdleme22f  33830  cdleme27cl  33850  cdlemefr27cl  33887