Theorem syl113anc 1378

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 399  df-3an 1085

This theorem is referenced by:  syl123anc  1383  syl213anc  1385  pythagtriplem18  16169  initoeu2  17276  psgnunilem1  18621  mulmarep1gsum1  21182  mulmarep1gsum2  21183  smadiadetlem4  21278  cramerimplem2  21293  cramerlem2  21297  cramer  21300  cnhaus  21962  dishaus  21990  ordthauslem  21991  pthaus  22246  txhaus  22255  xkohaus  22261  regr1lem  22347  methaus  23130  metnrmlem3  23469  iscgrad  26597  f1otrge  26658  axpaschlem  26726  wwlksnwwlksnon  27694  n4cyclfrgr  28070  br8d  30361  lt2addrd  30475  xlt2addrd  30482  br8  32992  br4  32994  nosupres  33207  nosupbnd1lem1  33208  nosupbnd2  33216  btwnxfr  33517  lineext  33537  brsegle  33569  brsegle2  33570  lfl0  36216  lfladd  36217  lflsub  36218  lflmul  36219  lflnegcl  36226  lflvscl  36228  lkrlss  36246  3dimlem3  36612  3dimlem4  36615  3dim3  36620  2llnm3N  36720  2lplnja  36770  4atex  37227  4atex3  37232  trlval4  37339  cdleme7c  37396  cdleme7d  37397  cdleme7ga  37399  cdleme21h  37485  cdleme21i  37486  cdleme21j  37487  cdleme21  37488  cdleme32d  37595  cdleme32f  37597  cdleme35h2  37608  cdleme38m  37614  cdleme40m  37618  cdlemg8  37782  cdlemg11a  37788  cdlemg10a  37791  cdlemg12b  37795  cdlemg12d  37797  cdlemg12f  37799  cdlemg12g  37800  cdlemg15a  37806  cdlemg16  37808  cdlemg16z  37810  cdlemg18a  37829  cdlemg24  37839  cdlemg29  37856  cdlemg33b  37858  cdlemg38  37866  cdlemg39  37867  cdlemg40  37868  cdlemg44b  37883  cdlemj2  37973  cdlemk7  37999  cdlemk12  38001  cdlemk12u  38023  cdlemk32  38048  cdlemk25-3  38055  cdlemk34  38061  cdlemkid3N  38084  cdlemkid4  38085  cdlemk11t  38097  cdlemk53  38108  cdlemk55b  38111  cdleml3N  38129  hdmapln1  39057