Theorem syl23anc 1226

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 1221	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  6829  suppofss2d  6830  cnfcomlem  8036  cnfcomlemOLD  8044  ackbij1lem16  8508  div2subd  10261  symg2bas  16014  evl1expd  17897  psgndiflemA  18149  oftpos  18453  restopn2  18906  tsmsxp  19854  blcld  20205  metustexhalfOLD  20263  metustexhalf  20264  cnllycmp  20653  dvlipcn  21592  tanregt0  22121  ostthlem1  23002  ax5seglem6  23325  axcontlem4  23358  axcontlem7  23361  pnfneige0  26519  qqhval2  26549  esumcocn  26667  heiborlem8  28858  mpaaeu  29648  wwlkextwrd  30501  bnj1125  32286  2atjm  33398  1cvrat  33429  lvolnlelln  33537  lvolnlelpln  33538  4atlem3  33549  lplncvrlvol  33569  dalem39  33664  cdleme4a  34192  cdleme15  34231  cdleme16c  34233  cdleme19b  34257  cdleme19e  34260  cdleme20d  34265  cdleme20g  34268  cdleme20j  34271  cdleme20k  34272  cdleme20l2  34274  cdleme20l  34275  cdleme20m  34276  cdleme22e  34297  cdleme22eALTN  34298  cdleme22f  34299  cdleme27cl  34319  cdlemefr27cl  34356