Theorem syl113anc 1380

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 395  df-3an 1087

This theorem is referenced by:  syl123anc  1385  syl213anc  1387  pythagtriplem18  16769  initoeu2  17970  psgnunilem1  19402  mulmarep1gsum1  22295  mulmarep1gsum2  22296  smadiadetlem4  22391  cramerimplem2  22406  cramerlem2  22410  cramer  22413  cnhaus  23078  dishaus  23106  ordthauslem  23107  pthaus  23362  txhaus  23371  xkohaus  23377  regr1lem  23463  methaus  24249  metnrmlem3  24597  nosupres  27446  nosupbnd1lem1  27447  nosupbnd2  27455  noinfres  27461  noinfbnd1lem1  27462  iscgrad  28329  f1otrge  28390  axpaschlem  28465  wwlksnwwlksnon  29436  n4cyclfrgr  29811  br8d  32106  lt2addrd  32231  xlt2addrd  32238  br8  35030  br4  35032  btwnxfr  35332  lineext  35352  brsegle  35384  brsegle2  35385  lfl0  38238  lfladd  38239  lflsub  38240  lflmul  38241  lflnegcl  38248  lflvscl  38250  lkrlss  38268  3dimlem3  38635  3dimlem4  38638  3dim3  38643  2llnm3N  38743  2lplnja  38793  4atex  39250  4atex3  39255  trlval4  39362  cdleme7c  39419  cdleme7d  39420  cdleme7ga  39422  cdleme21h  39508  cdleme21i  39509  cdleme21j  39510  cdleme21  39511  cdleme32d  39618  cdleme32f  39620  cdleme35h2  39631  cdleme38m  39637  cdleme40m  39641  cdlemg8  39805  cdlemg11a  39811  cdlemg10a  39814  cdlemg12b  39818  cdlemg12d  39820  cdlemg12f  39822  cdlemg12g  39823  cdlemg15a  39829  cdlemg16  39831  cdlemg16z  39833  cdlemg18a  39852  cdlemg24  39862  cdlemg29  39879  cdlemg33b  39881  cdlemg38  39889  cdlemg39  39890  cdlemg40  39891  cdlemg44b  39906  cdlemj2  39996  cdlemk7  40022  cdlemk12  40024  cdlemk12u  40046  cdlemk32  40071  cdlemk25-3  40078  cdlemk34  40084  cdlemkid3N  40107  cdlemkid4  40108  cdlemk11t  40120  cdlemk53  40131  cdlemk55b  40134  cdleml3N  40152  hdmapln1  41080  tfsconcatrev  42400  sepfsepc  47647