Theorem syl113anc 1381

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  syl123anc  1386  syl213anc  1388  hash7g  14522  pythagtriplem18  16866  initoeu2  18070  psgnunilem1  19526  mulmarep1gsum1  22595  mulmarep1gsum2  22596  smadiadetlem4  22691  cramerimplem2  22706  cramerlem2  22710  cramer  22713  cnhaus  23378  dishaus  23406  ordthauslem  23407  pthaus  23662  txhaus  23671  xkohaus  23677  regr1lem  23763  methaus  24549  metnrmlem3  24897  nosupres  27767  nosupbnd1lem1  27768  nosupbnd2  27776  noinfres  27782  noinfbnd1lem1  27783  iscgrad  28834  f1otrge  28895  axpaschlem  28970  wwlksnwwlksnon  29945  n4cyclfrgr  30320  br8d  32630  lt2addrd  32762  xlt2addrd  32769  br8  35736  br4  35738  btwnxfr  36038  lineext  36058  brsegle  36090  brsegle2  36091  lfl0  39047  lfladd  39048  lflsub  39049  lflmul  39050  lflnegcl  39057  lflvscl  39059  lkrlss  39077  3dimlem3  39444  3dimlem4  39447  3dim3  39452  2llnm3N  39552  2lplnja  39602  4atex  40059  4atex3  40064  trlval4  40171  cdleme7c  40228  cdleme7d  40229  cdleme7ga  40231  cdleme21h  40317  cdleme21i  40318  cdleme21j  40319  cdleme21  40320  cdleme32d  40427  cdleme32f  40429  cdleme35h2  40440  cdleme38m  40446  cdleme40m  40450  cdlemg8  40614  cdlemg11a  40620  cdlemg10a  40623  cdlemg12b  40627  cdlemg12d  40629  cdlemg12f  40631  cdlemg12g  40632  cdlemg15a  40638  cdlemg16  40640  cdlemg16z  40642  cdlemg18a  40661  cdlemg24  40671  cdlemg29  40688  cdlemg33b  40690  cdlemg38  40698  cdlemg39  40699  cdlemg40  40700  cdlemg44b  40715  cdlemj2  40805  cdlemk7  40831  cdlemk12  40833  cdlemk12u  40855  cdlemk32  40880  cdlemk25-3  40887  cdlemk34  40893  cdlemkid3N  40916  cdlemkid4  40917  cdlemk11t  40929  cdlemk53  40940  cdlemk55b  40943  cdleml3N  40961  hdmapln1  41889  tfsconcatrev  43338  isubgr3stgrlem6  47874  sepfsepc  48724