Theorem syl113anc 1400

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

Syntax hints:   → wi 4   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  syl123anc  1405  syl213anc  1407  hash7g  14496  pythagtriplem18  16851  initoeu2  18032  psgnunilem1  19516  mulmarep1gsum1  22613  mulmarep1gsum2  22614  smadiadetlem4  22709  cramerimplem2  22724  cramerlem2  22728  cramer  22731  cnhaus  23394  dishaus  23422  ordthauslem  23423  pthaus  23678  txhaus  23687  xkohaus  23693  regr1lem  23779  methaus  24560  metnrmlem3  24902  nosupres  27748  nosupbnd1lem1  27749  nosupbnd2  27757  noinfres  27763  noinfbnd1lem1  27764  iscgrad  28957  f1otrge  29018  axpaschlem  29087  wwlksnwwlksnon  30061  n4cyclfrgr  30439  br8d  32760  lt2addrd  32902  xlt2addrd  32911  br8  36070  br4  36072  btwnxfr  36370  lineext  36390  brsegle  36422  brsegle2  36423  lfl0  39653  lfladd  39654  lflsub  39655  lflmul  39656  lflnegcl  39663  lflvscl  39665  lkrlss  39683  3dimlem3  40049  3dimlem4  40052  3dim3  40057  2llnm3N  40157  2lplnja  40207  4atex  40664  4atex3  40669  trlval4  40776  cdleme7c  40833  cdleme7d  40834  cdleme7ga  40836  cdleme21h  40922  cdleme21i  40923  cdleme21j  40924  cdleme21  40925  cdleme32d  41032  cdleme32f  41034  cdleme35h2  41045  cdleme38m  41051  cdleme40m  41055  cdlemg8  41219  cdlemg11a  41225  cdlemg10a  41228  cdlemg12b  41232  cdlemg12d  41234  cdlemg12f  41236  cdlemg12g  41237  cdlemg15a  41243  cdlemg16  41245  cdlemg16z  41247  cdlemg18a  41266  cdlemg24  41276  cdlemg29  41293  cdlemg33b  41295  cdlemg38  41303  cdlemg39  41304  cdlemg40  41305  cdlemg44b  41320  cdlemj2  41410  cdlemk7  41436  cdlemk12  41438  cdlemk12u  41460  cdlemk32  41485  cdlemk25-3  41492  cdlemk34  41498  cdlemkid3N  41521  cdlemkid4  41522  cdlemk11t  41534  cdlemk53  41545  cdlemk55b  41548  cdleml3N  41566  hdmapln1  42494  tfsconcatrev  43889  isubgr3stgrlem6  48557  sepfsepc  49513