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

This theorem is referenced by:  syl123anc  1386  syl213anc  1388  pythagtriplem18  16770  initoeu2  17971  psgnunilem1  19403  mulmarep1gsum1  22296  mulmarep1gsum2  22297  smadiadetlem4  22392  cramerimplem2  22407  cramerlem2  22411  cramer  22414  cnhaus  23079  dishaus  23107  ordthauslem  23108  pthaus  23363  txhaus  23372  xkohaus  23378  regr1lem  23464  methaus  24250  metnrmlem3  24598  nosupres  27447  nosupbnd1lem1  27448  nosupbnd2  27456  noinfres  27462  noinfbnd1lem1  27463  iscgrad  28330  f1otrge  28391  axpaschlem  28466  wwlksnwwlksnon  29437  n4cyclfrgr  29812  br8d  32107  lt2addrd  32232  xlt2addrd  32239  br8  35031  br4  35033  btwnxfr  35333  lineext  35353  brsegle  35385  brsegle2  35386  lfl0  38239  lfladd  38240  lflsub  38241  lflmul  38242  lflnegcl  38249  lflvscl  38251  lkrlss  38269  3dimlem3  38636  3dimlem4  38639  3dim3  38644  2llnm3N  38744  2lplnja  38794  4atex  39251  4atex3  39256  trlval4  39363  cdleme7c  39420  cdleme7d  39421  cdleme7ga  39423  cdleme21h  39509  cdleme21i  39510  cdleme21j  39511  cdleme21  39512  cdleme32d  39619  cdleme32f  39621  cdleme35h2  39632  cdleme38m  39638  cdleme40m  39642  cdlemg8  39806  cdlemg11a  39812  cdlemg10a  39815  cdlemg12b  39819  cdlemg12d  39821  cdlemg12f  39823  cdlemg12g  39824  cdlemg15a  39830  cdlemg16  39832  cdlemg16z  39834  cdlemg18a  39853  cdlemg24  39863  cdlemg29  39880  cdlemg33b  39882  cdlemg38  39890  cdlemg39  39891  cdlemg40  39892  cdlemg44b  39907  cdlemj2  39997  cdlemk7  40023  cdlemk12  40025  cdlemk12u  40047  cdlemk32  40072  cdlemk25-3  40079  cdlemk34  40085  cdlemkid3N  40108  cdlemkid4  40109  cdlemk11t  40121  cdlemk53  40132  cdlemk55b  40135  cdleml3N  40153  hdmapln1  41081  tfsconcatrev  42401  sepfsepc  47648