Theorem syl113anc 1338

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

Assertion

Ref	Expression
syl113anc	|- ( ph -> ze )

Proof of Theorem syl113anc

Step	Hyp	Ref	Expression
1		syl12anc.1	. 2 |- ( ph -> ps )
2		syl12anc.2	. 2 |- ( ph -> ch )
3		syl12anc.3	. . 3 |- ( ph -> th )
4		syl22anc.4	. . 3 |- ( ph -> ta )
5		syl23anc.5	. . 3 |- ( ph -> et )
6	3, 4, 5	3jca 1242	. 2 |- ( ph -> ( th /\ ta /\ et ) )
7		syl113anc.6	. 2 |- ( ( ps /\ ch /\ ( th /\ ta /\ et ) ) -> ze )
8	1, 2, 6, 7	syl3anc 1326	1 |- ( ph -> ze )

Syntax hints:   -> wi 4   /\ 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:  syl123anc  1343  syl213anc  1345  pythagtriplem18  15537  initoeu2  16666  psgnunilem1  17913  mulmarep1gsum1  20379  mulmarep1gsum2  20380  smadiadetlem4  20475  cramerimplem2  20490  cramerlem2  20494  cramer  20497  cnhaus  21158  dishaus  21186  ordthauslem  21187  pthaus  21441  txhaus  21450  xkohaus  21456  regr1lem  21542  methaus  22325  metnrmlem3  22664  f1otrge  25752  axpaschlem  25820  wwlksnwwlksnon  26810  n4cyclfrgr  27155  br8d  29422  lt2addrd  29516  xlt2addrd  29523  br8  31646  br4  31648  nosupres  31853  nosupbnd1lem1  31854  nosupbnd2  31862  btwnxfr  32163  lineext  32183  brsegle  32215  brsegle2  32216  lfl0  34352  lfladd  34353  lflsub  34354  lflmul  34355  lflnegcl  34362  lflvscl  34364  lkrlss  34382  3dimlem3  34747  3dimlem4  34750  3dim3  34755  2llnm3N  34855  2lplnja  34905  4atex  35362  4atex3  35367  trlval4  35475  cdleme7c  35532  cdleme7d  35533  cdleme7ga  35535  cdleme21h  35622  cdleme21i  35623  cdleme21j  35624  cdleme21  35625  cdleme32d  35732  cdleme32f  35734  cdleme35h2  35745  cdleme38m  35751  cdleme40m  35755  cdlemg8  35919  cdlemg11a  35925  cdlemg10a  35928  cdlemg12b  35932  cdlemg12d  35934  cdlemg12f  35936  cdlemg12g  35937  cdlemg15a  35943  cdlemg16  35945  cdlemg16z  35947  cdlemg18a  35966  cdlemg24  35976  cdlemg29  35993  cdlemg33b  35995  cdlemg38  36003  cdlemg39  36004  cdlemg40  36005  cdlemg44b  36020  cdlemj2  36110  cdlemk7  36136  cdlemk12  36138  cdlemk12u  36160  cdlemk32  36185  cdlemk25-3  36192  cdlemk34  36198  cdlemkid3N  36221  cdlemkid4  36222  cdlemk11t  36234  cdlemk53  36245  cdlemk55b  36248  cdleml3N  36266  hdmapln1  37198