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  14411  pythagtriplem18  16762  initoeu2  17941  psgnunilem1  19390  mulmarep1gsum1  22476  mulmarep1gsum2  22477  smadiadetlem4  22572  cramerimplem2  22587  cramerlem2  22591  cramer  22594  cnhaus  23257  dishaus  23285  ordthauslem  23286  pthaus  23541  txhaus  23550  xkohaus  23556  regr1lem  23642  methaus  24424  metnrmlem3  24766  nosupres  27635  nosupbnd1lem1  27636  nosupbnd2  27644  noinfres  27650  noinfbnd1lem1  27651  iscgrad  28774  f1otrge  28835  axpaschlem  28903  wwlksnwwlksnon  29878  n4cyclfrgr  30253  br8d  32571  lt2addrd  32707  xlt2addrd  32715  br8  35728  br4  35730  btwnxfr  36029  lineext  36049  brsegle  36081  brsegle2  36082  lfl0  39043  lfladd  39044  lflsub  39045  lflmul  39046  lflnegcl  39053  lflvscl  39055  lkrlss  39073  3dimlem3  39440  3dimlem4  39443  3dim3  39448  2llnm3N  39548  2lplnja  39598  4atex  40055  4atex3  40060  trlval4  40167  cdleme7c  40224  cdleme7d  40225  cdleme7ga  40227  cdleme21h  40313  cdleme21i  40314  cdleme21j  40315  cdleme21  40316  cdleme32d  40423  cdleme32f  40425  cdleme35h2  40436  cdleme38m  40442  cdleme40m  40446  cdlemg8  40610  cdlemg11a  40616  cdlemg10a  40619  cdlemg12b  40623  cdlemg12d  40625  cdlemg12f  40627  cdlemg12g  40628  cdlemg15a  40634  cdlemg16  40636  cdlemg16z  40638  cdlemg18a  40657  cdlemg24  40667  cdlemg29  40684  cdlemg33b  40686  cdlemg38  40694  cdlemg39  40695  cdlemg40  40696  cdlemg44b  40711  cdlemj2  40801  cdlemk7  40827  cdlemk12  40829  cdlemk12u  40851  cdlemk32  40876  cdlemk25-3  40883  cdlemk34  40889  cdlemkid3N  40912  cdlemkid4  40913  cdlemk11t  40925  cdlemk53  40936  cdlemk55b  40939  cdleml3N  40957  hdmapln1  41885  tfsconcatrev  43321  isubgr3stgrlem6  47956  sepfsepc  48913