Theorem syl23anc 1239

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 1234	1 |- ( ph -> ze )

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

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 187  df-an 371  df-3an 978

This theorem is referenced by:  suppofss1d  6942  suppofss2d  6943  cnfcomlem  8177  cnfcomlemOLD  8185  ackbij1lem16  8649  div2subd  10413  symg2bas  16749  evl1expd  18703  psgndiflemA  18937  oftpos  19248  restopn2  19973  tsmsxp  20951  blcld  21302  metustexhalfOLD  21360  metustexhalf  21361  cnllycmp  21750  dvlipcn  22689  tanregt0  23220  ostthlem1  24195  ax5seglem6  24666  axcontlem4  24699  axcontlem7  24702  wwlkextwrd  25157  pnfneige0  28399  qqhval2  28428  esumcocn  28540  carsgmon  28775  bnj1125  29388  heiborlem8  31609  2atjm  32475  1cvrat  32506  lvolnlelln  32614  lvolnlelpln  32615  4atlem3  32626  lplncvrlvol  32646  dalem39  32741  cdleme4a  33270  cdleme15  33309  cdleme16c  33311  cdleme19b  33336  cdleme19e  33339  cdleme20d  33344  cdleme20g  33347  cdleme20j  33350  cdleme20k  33351  cdleme20l2  33353  cdleme20l  33354  cdleme20m  33355  cdleme22e  33376  cdleme22eALTN  33377  cdleme22f  33378  cdleme27cl  33398  cdlemefr27cl  33435  mpaaeu  35476