Theorem syl113anc 1405

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  syl123anc  1410  syl213anc  1412  hash7g  14513  pythagtriplem18  16882  initoeu2  18063  psgnunilem1  19554  mulmarep1gsum1  22691  mulmarep1gsum2  22692  smadiadetlem4  22787  cramerimplem2  22802  cramerlem2  22806  cramer  22809  cnhaus  23472  dishaus  23500  ordthauslem  23501  pthaus  23756  txhaus  23765  xkohaus  23771  regr1lem  23857  methaus  24638  metnrmlem3  24980  nosupres  27829  nosupbnd1lem1  27830  nosupbnd2  27838  noinfres  27844  noinfbnd1lem1  27845  iscgrad  29063  f1otrge  29130  axpaschlem  29199  wwlksnwwlksnon  30173  n4cyclfrgr  30551  br8d  32865  lt2addrd  33007  xlt2addrd  33016  br8  36119  br4  36121  btwnxfr  36419  lineext  36439  brsegle  36471  brsegle2  36472  lfl0  39701  lfladd  39702  lflsub  39703  lflmul  39704  lflnegcl  39711  lflvscl  39713  lkrlss  39731  3dimlem3  40097  3dimlem4  40100  3dim3  40105  2llnm3N  40205  2lplnja  40255  4atex  40712  4atex3  40717  trlval4  40824  cdleme7c  40881  cdleme7d  40882  cdleme7ga  40884  cdleme21h  40970  cdleme21i  40971  cdleme21j  40972  cdleme21  40973  cdleme32d  41080  cdleme32f  41082  cdleme35h2  41093  cdleme38m  41099  cdleme40m  41103  cdlemg8  41267  cdlemg11a  41273  cdlemg10a  41276  cdlemg12b  41280  cdlemg12d  41282  cdlemg12f  41284  cdlemg12g  41285  cdlemg15a  41291  cdlemg16  41293  cdlemg16z  41295  cdlemg18a  41314  cdlemg24  41324  cdlemg29  41341  cdlemg33b  41343  cdlemg38  41351  cdlemg39  41352  cdlemg40  41353  cdlemg44b  41368  cdlemj2  41458  cdlemk7  41484  cdlemk12  41486  cdlemk12u  41508  cdlemk32  41533  cdlemk25-3  41540  cdlemk34  41546  cdlemkid3N  41569  cdlemkid4  41570  cdlemk11t  41582  cdlemk53  41593  cdlemk55b  41596  cdleml3N  41614  hdmapln1  42542  tfsconcatrev  43937  isubgr3stgrlem6  48591  sepfsepc  49557