Theorem syl113anc 1409

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  syl123anc  1414  syl213anc  1416  hash7g  14555  pythagtriplem18  16930  initoeu2  18111  psgnunilem1  19626  mulmarep1gsum1  22801  mulmarep1gsum2  22802  smadiadetlem4  22897  cramerimplem2  22915  cramerlem2  22919  cramer  22922  cnhaus  23585  dishaus  23613  ordthauslem  23614  pthaus  23870  txhaus  23879  xkohaus  23885  regr1lem  23971  methaus  24752  metnrmlem3  25094  nosupres  27951  nosupbnd1lem1  27952  nosupbnd2  27960  noinfres  27966  noinfbnd1lem1  27967  iscgrad  29205  f1otrge  29336  axpaschlem  29405  wwlksnwwlksnon  30391  n4cyclfrgr  30779  br8d  33089  lt2addrd  33229  xlt2addrd  33238  br8  36343  br4  36345  btwnxfr  36644  lineext  36664  brsegle  36696  brsegle2  36697  lfl0  39946  lfladd  39947  lflsub  39948  lflmul  39949  lflnegcl  39956  lflvscl  39958  lkrlss  39976  3dimlem3  40342  3dimlem4  40345  3dim3  40350  2llnm3N  40450  2lplnja  40500  4atex  40957  4atex3  40962  trlval4  41069  cdleme7c  41126  cdleme7d  41127  cdleme7ga  41129  cdleme21h  41215  cdleme21i  41216  cdleme21j  41217  cdleme21  41218  cdleme32d  41325  cdleme32f  41327  cdleme35h2  41338  cdleme38m  41344  cdleme40m  41348  cdlemg8  41512  cdlemg11a  41518  cdlemg10a  41521  cdlemg12b  41525  cdlemg12d  41527  cdlemg12f  41529  cdlemg12g  41530  cdlemg15a  41536  cdlemg16  41538  cdlemg16z  41540  cdlemg18a  41559  cdlemg24  41569  cdlemg29  41586  cdlemg33b  41588  cdlemg38  41596  cdlemg39  41597  cdlemg40  41598  cdlemg44b  41613  cdlemj2  41703  cdlemk7  41729  cdlemk12  41731  cdlemk12u  41753  cdlemk32  41778  cdlemk25-3  41785  cdlemk34  41791  cdlemkid3N  41814  cdlemkid4  41815  cdlemk11t  41827  cdlemk53  41838  cdlemk55b  41841  cdleml3N  41859  hdmapln1  42787  tfsconcatrev  44197  isubgr3stgrlem6  48895  sepfsepc  49862