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  14634  pythagtriplem18  17015  initoeu2  18196  psgnunilem1  19712  mulmarep1gsum1  22893  mulmarep1gsum2  22894  smadiadetlem4  22989  cramerimplem2  23007  cramerlem2  23011  cramer  23014  cnhaus  23677  dishaus  23705  ordthauslem  23706  pthaus  23962  txhaus  23971  xkohaus  23977  regr1lem  24063  methaus  24844  metnrmlem3  25186  nosupres  28069  nosupbnd1lem1  28070  nosupbnd2  28078  noinfres  28084  noinfbnd1lem1  28085  iscgrad  29323  f1otrge  29454  axpaschlem  29523  wwlksnwwlksnon  30509  n4cyclfrgr  30897  br8d  33249  lt2addrd  33388  xlt2addrd  33397  br8  36613  br4  36615  btwnxfr  36913  lineext  36933  brsegle  36965  brsegle2  36966  lfl0  40215  lfladd  40216  lflsub  40217  lflmul  40218  lflnegcl  40225  lflvscl  40227  lkrlss  40245  3dimlem3  40611  3dimlem4  40614  3dim3  40619  2llnm3N  40719  2lplnja  40769  4atex  41226  4atex3  41231  trlval4  41338  cdleme7c  41395  cdleme7d  41396  cdleme7ga  41398  cdleme21h  41484  cdleme21i  41485  cdleme21j  41486  cdleme21  41487  cdleme32d  41594  cdleme32f  41596  cdleme35h2  41607  cdleme38m  41613  cdleme40m  41617  cdlemg8  41781  cdlemg11a  41787  cdlemg10a  41790  cdlemg12b  41794  cdlemg12d  41796  cdlemg12f  41798  cdlemg12g  41799  cdlemg15a  41805  cdlemg16  41807  cdlemg16z  41809  cdlemg18a  41828  cdlemg24  41838  cdlemg29  41855  cdlemg33b  41857  cdlemg38  41865  cdlemg39  41866  cdlemg40  41867  cdlemg44b  41882  cdlemj2  41972  cdlemk7  41998  cdlemk12  42000  cdlemk12u  42022  cdlemk32  42047  cdlemk25-3  42054  cdlemk34  42060  cdlemkid3N  42083  cdlemkid4  42084  cdlemk11t  42096  cdlemk53  42107  cdlemk55b  42110  cdleml3N  42128  hdmapln1  43056  tfsconcatrev  44443  isubgr3stgrlem6  49162  sepfsepc  50135