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  14543  pythagtriplem18  16917  initoeu2  18098  psgnunilem1  19594  mulmarep1gsum1  22767  mulmarep1gsum2  22768  smadiadetlem4  22863  cramerimplem2  22878  cramerlem2  22882  cramer  22885  cnhaus  23548  dishaus  23576  ordthauslem  23577  pthaus  23832  txhaus  23841  xkohaus  23847  regr1lem  23933  methaus  24714  metnrmlem3  25056  nosupres  27908  nosupbnd1lem1  27909  nosupbnd2  27917  noinfres  27923  noinfbnd1lem1  27924  iscgrad  29159  f1otrge  29258  axpaschlem  29327  wwlksnwwlksnon  30301  n4cyclfrgr  30679  br8d  32990  lt2addrd  33132  xlt2addrd  33141  br8  36269  br4  36271  btwnxfr  36569  lineext  36589  brsegle  36621  brsegle2  36622  lfl0  39880  lfladd  39881  lflsub  39882  lflmul  39883  lflnegcl  39890  lflvscl  39892  lkrlss  39910  3dimlem3  40276  3dimlem4  40279  3dim3  40284  2llnm3N  40384  2lplnja  40434  4atex  40891  4atex3  40896  trlval4  41003  cdleme7c  41060  cdleme7d  41061  cdleme7ga  41063  cdleme21h  41149  cdleme21i  41150  cdleme21j  41151  cdleme21  41152  cdleme32d  41259  cdleme32f  41261  cdleme35h2  41272  cdleme38m  41278  cdleme40m  41282  cdlemg8  41446  cdlemg11a  41452  cdlemg10a  41455  cdlemg12b  41459  cdlemg12d  41461  cdlemg12f  41463  cdlemg12g  41464  cdlemg15a  41470  cdlemg16  41472  cdlemg16z  41474  cdlemg18a  41493  cdlemg24  41503  cdlemg29  41520  cdlemg33b  41522  cdlemg38  41530  cdlemg39  41531  cdlemg40  41532  cdlemg44b  41547  cdlemj2  41637  cdlemk7  41663  cdlemk12  41665  cdlemk12u  41687  cdlemk32  41712  cdlemk25-3  41719  cdlemk34  41725  cdlemkid3N  41748  cdlemkid4  41749  cdlemk11t  41761  cdlemk53  41772  cdlemk55b  41775  cdleml3N  41793  hdmapln1  42721  tfsconcatrev  44116  isubgr3stgrlem6  48777  sepfsepc  49747