Theorem syl23anc 1235

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

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

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 975

This theorem is referenced by:  suppofss1d  6934  suppofss2d  6935  cnfcomlem  8139  cnfcomlemOLD  8147  ackbij1lem16  8611  div2subd  10366  symg2bas  16218  evl1expd  18152  psgndiflemA  18404  oftpos  18721  restopn2  19444  tsmsxp  20392  blcld  20743  metustexhalfOLD  20801  metustexhalf  20802  cnllycmp  21191  dvlipcn  22130  tanregt0  22659  ostthlem1  23540  ax5seglem6  23913  axcontlem4  23946  axcontlem7  23949  wwlkextwrd  24404  pnfneige0  27569  qqhval2  27599  esumcocn  27726  heiborlem8  29917  mpaaeu  30704  bnj1125  33127  2atjm  34241  1cvrat  34272  lvolnlelln  34380  lvolnlelpln  34381  4atlem3  34392  lplncvrlvol  34412  dalem39  34507  cdleme4a  35035  cdleme15  35074  cdleme16c  35076  cdleme19b  35100  cdleme19e  35103  cdleme20d  35108  cdleme20g  35111  cdleme20j  35114  cdleme20k  35115  cdleme20l2  35117  cdleme20l  35118  cdleme20m  35119  cdleme22e  35140  cdleme22eALTN  35141  cdleme22f  35142  cdleme27cl  35162  cdlemefr27cl  35199