Theorem syl113anc 1379

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
syl3anc.1	⊢ (𝜑 → 𝜓)
syl3anc.2	⊢ (𝜑 → 𝜒)
syl3anc.3	⊢ (𝜑 → 𝜃)
syl3Xanc.4	⊢ (𝜑 → 𝜏)
syl23anc.5	⊢ (𝜑 → 𝜂)
syl113anc.6	⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁)

Assertion

Ref	Expression
syl113anc	⊢ (𝜑 → 𝜁)

Proof of Theorem syl113anc

Step	Hyp	Ref	Expression
1		syl3anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl3anc.2	. 2 ⊢ (𝜑 → 𝜒)
3		syl3anc.3	. . 3 ⊢ (𝜑 → 𝜃)
4		syl3Xanc.4	. . 3 ⊢ (𝜑 → 𝜏)
5		syl23anc.5	. . 3 ⊢ (𝜑 → 𝜂)
6	3, 4, 5	3jca 1125	. 2 ⊢ (𝜑 → (𝜃 ∧ 𝜏 ∧ 𝜂))
7		syl113anc.6	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁)
8	1, 2, 6, 7	syl3anc 1368	1 ⊢ (𝜑 → 𝜁)

Syntax hints:   → wi 4   ∧ w3a 1084

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 206  df-an 396  df-3an 1086

This theorem is referenced by:  syl123anc  1384  syl213anc  1386  pythagtriplem18  16764  initoeu2  17968  psgnunilem1  19403  mulmarep1gsum1  22397  mulmarep1gsum2  22398  smadiadetlem4  22493  cramerimplem2  22508  cramerlem2  22512  cramer  22515  cnhaus  23180  dishaus  23208  ordthauslem  23209  pthaus  23464  txhaus  23473  xkohaus  23479  regr1lem  23565  methaus  24351  metnrmlem3  24699  nosupres  27556  nosupbnd1lem1  27557  nosupbnd2  27565  noinfres  27571  noinfbnd1lem1  27572  iscgrad  28531  f1otrge  28592  axpaschlem  28667  wwlksnwwlksnon  29638  n4cyclfrgr  30013  br8d  32308  lt2addrd  32433  xlt2addrd  32440  br8  35221  br4  35223  btwnxfr  35523  lineext  35543  brsegle  35575  brsegle2  35576  lfl0  38425  lfladd  38426  lflsub  38427  lflmul  38428  lflnegcl  38435  lflvscl  38437  lkrlss  38455  3dimlem3  38822  3dimlem4  38825  3dim3  38830  2llnm3N  38930  2lplnja  38980  4atex  39437  4atex3  39442  trlval4  39549  cdleme7c  39606  cdleme7d  39607  cdleme7ga  39609  cdleme21h  39695  cdleme21i  39696  cdleme21j  39697  cdleme21  39698  cdleme32d  39805  cdleme32f  39807  cdleme35h2  39818  cdleme38m  39824  cdleme40m  39828  cdlemg8  39992  cdlemg11a  39998  cdlemg10a  40001  cdlemg12b  40005  cdlemg12d  40007  cdlemg12f  40009  cdlemg12g  40010  cdlemg15a  40016  cdlemg16  40018  cdlemg16z  40020  cdlemg18a  40039  cdlemg24  40049  cdlemg29  40066  cdlemg33b  40068  cdlemg38  40076  cdlemg39  40077  cdlemg40  40078  cdlemg44b  40093  cdlemj2  40183  cdlemk7  40209  cdlemk12  40211  cdlemk12u  40233  cdlemk32  40258  cdlemk25-3  40265  cdlemk34  40271  cdlemkid3N  40294  cdlemkid4  40295  cdlemk11t  40307  cdlemk53  40318  cdlemk55b  40321  cdleml3N  40339  hdmapln1  41267  tfsconcatrev  42587  sepfsepc  47748