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  14611  pythagtriplem18  16990  initoeu2  18171  psgnunilem1  19687  mulmarep1gsum1  22868  mulmarep1gsum2  22869  smadiadetlem4  22964  cramerimplem2  22982  cramerlem2  22986  cramer  22989  cnhaus  23652  dishaus  23680  ordthauslem  23681  pthaus  23937  txhaus  23946  xkohaus  23952  regr1lem  24038  methaus  24819  metnrmlem3  25161  nosupres  28046  nosupbnd1lem1  28047  nosupbnd2  28055  noinfres  28061  noinfbnd1lem1  28062  iscgrad  29300  f1otrge  29431  axpaschlem  29500  wwlksnwwlksnon  30486  n4cyclfrgr  30874  br8d  33184  lt2addrd  33324  xlt2addrd  33333  br8  36490  br4  36492  btwnxfr  36791  lineext  36811  brsegle  36843  brsegle2  36844  lfl0  40090  lfladd  40091  lflsub  40092  lflmul  40093  lflnegcl  40100  lflvscl  40102  lkrlss  40120  3dimlem3  40486  3dimlem4  40489  3dim3  40494  2llnm3N  40594  2lplnja  40644  4atex  41101  4atex3  41106  trlval4  41213  cdleme7c  41270  cdleme7d  41271  cdleme7ga  41273  cdleme21h  41359  cdleme21i  41360  cdleme21j  41361  cdleme21  41362  cdleme32d  41469  cdleme32f  41471  cdleme35h2  41482  cdleme38m  41488  cdleme40m  41492  cdlemg8  41656  cdlemg11a  41662  cdlemg10a  41665  cdlemg12b  41669  cdlemg12d  41671  cdlemg12f  41673  cdlemg12g  41674  cdlemg15a  41680  cdlemg16  41682  cdlemg16z  41684  cdlemg18a  41703  cdlemg24  41713  cdlemg29  41730  cdlemg33b  41732  cdlemg38  41740  cdlemg39  41741  cdlemg40  41742  cdlemg44b  41757  cdlemj2  41847  cdlemk7  41873  cdlemk12  41875  cdlemk12u  41897  cdlemk32  41922  cdlemk25-3  41929  cdlemk34  41935  cdlemkid3N  41958  cdlemkid4  41959  cdlemk11t  41971  cdlemk53  41982  cdlemk55b  41985  cdleml3N  42003  hdmapln1  42931  tfsconcatrev  44308  isubgr3stgrlem6  49013  sepfsepc  49980