Theorem syl113anc 1384

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 1128	. 2 ⊢ (𝜑 → (𝜃 ∧ 𝜏 ∧ 𝜂))
7		syl113anc.6	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁)
8	1, 2, 6, 7	syl3anc 1373	1 ⊢ (𝜑 → 𝜁)

Syntax hints:   → wi 4   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  syl123anc  1389  syl213anc  1391  hash7g  14458  pythagtriplem18  16810  initoeu2  17985  psgnunilem1  19430  mulmarep1gsum1  22467  mulmarep1gsum2  22468  smadiadetlem4  22563  cramerimplem2  22578  cramerlem2  22582  cramer  22585  cnhaus  23248  dishaus  23276  ordthauslem  23277  pthaus  23532  txhaus  23541  xkohaus  23547  regr1lem  23633  methaus  24415  metnrmlem3  24757  nosupres  27626  nosupbnd1lem1  27627  nosupbnd2  27635  noinfres  27641  noinfbnd1lem1  27642  iscgrad  28745  f1otrge  28806  axpaschlem  28874  wwlksnwwlksnon  29852  n4cyclfrgr  30227  br8d  32545  lt2addrd  32681  xlt2addrd  32689  br8  35750  br4  35752  btwnxfr  36051  lineext  36071  brsegle  36103  brsegle2  36104  lfl0  39065  lfladd  39066  lflsub  39067  lflmul  39068  lflnegcl  39075  lflvscl  39077  lkrlss  39095  3dimlem3  39462  3dimlem4  39465  3dim3  39470  2llnm3N  39570  2lplnja  39620  4atex  40077  4atex3  40082  trlval4  40189  cdleme7c  40246  cdleme7d  40247  cdleme7ga  40249  cdleme21h  40335  cdleme21i  40336  cdleme21j  40337  cdleme21  40338  cdleme32d  40445  cdleme32f  40447  cdleme35h2  40458  cdleme38m  40464  cdleme40m  40468  cdlemg8  40632  cdlemg11a  40638  cdlemg10a  40641  cdlemg12b  40645  cdlemg12d  40647  cdlemg12f  40649  cdlemg12g  40650  cdlemg15a  40656  cdlemg16  40658  cdlemg16z  40660  cdlemg18a  40679  cdlemg24  40689  cdlemg29  40706  cdlemg33b  40708  cdlemg38  40716  cdlemg39  40717  cdlemg40  40718  cdlemg44b  40733  cdlemj2  40823  cdlemk7  40849  cdlemk12  40851  cdlemk12u  40873  cdlemk32  40898  cdlemk25-3  40905  cdlemk34  40911  cdlemkid3N  40934  cdlemkid4  40935  cdlemk11t  40947  cdlemk53  40958  cdlemk55b  40961  cdleml3N  40979  hdmapln1  41907  tfsconcatrev  43344  isubgr3stgrlem6  47974  sepfsepc  48920