Theorem syl113anc 1382

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  syl123anc  1387  syl213anc  1389  hash7g  14535  pythagtriplem18  16879  initoeu2  18083  psgnunilem1  19535  mulmarep1gsum1  22600  mulmarep1gsum2  22601  smadiadetlem4  22696  cramerimplem2  22711  cramerlem2  22715  cramer  22718  cnhaus  23383  dishaus  23411  ordthauslem  23412  pthaus  23667  txhaus  23676  xkohaus  23682  regr1lem  23768  methaus  24554  metnrmlem3  24902  nosupres  27770  nosupbnd1lem1  27771  nosupbnd2  27779  noinfres  27785  noinfbnd1lem1  27786  iscgrad  28837  f1otrge  28898  axpaschlem  28973  wwlksnwwlksnon  29948  n4cyclfrgr  30323  br8d  32632  lt2addrd  32758  xlt2addrd  32765  br8  35718  br4  35720  btwnxfr  36020  lineext  36040  brsegle  36072  brsegle2  36073  lfl0  39021  lfladd  39022  lflsub  39023  lflmul  39024  lflnegcl  39031  lflvscl  39033  lkrlss  39051  3dimlem3  39418  3dimlem4  39421  3dim3  39426  2llnm3N  39526  2lplnja  39576  4atex  40033  4atex3  40038  trlval4  40145  cdleme7c  40202  cdleme7d  40203  cdleme7ga  40205  cdleme21h  40291  cdleme21i  40292  cdleme21j  40293  cdleme21  40294  cdleme32d  40401  cdleme32f  40403  cdleme35h2  40414  cdleme38m  40420  cdleme40m  40424  cdlemg8  40588  cdlemg11a  40594  cdlemg10a  40597  cdlemg12b  40601  cdlemg12d  40603  cdlemg12f  40605  cdlemg12g  40606  cdlemg15a  40612  cdlemg16  40614  cdlemg16z  40616  cdlemg18a  40635  cdlemg24  40645  cdlemg29  40662  cdlemg33b  40664  cdlemg38  40672  cdlemg39  40673  cdlemg40  40674  cdlemg44b  40689  cdlemj2  40779  cdlemk7  40805  cdlemk12  40807  cdlemk12u  40829  cdlemk32  40854  cdlemk25-3  40861  cdlemk34  40867  cdlemkid3N  40890  cdlemkid4  40891  cdlemk11t  40903  cdlemk53  40914  cdlemk55b  40917  cdleml3N  40935  hdmapln1  41863  tfsconcatrev  43310  sepfsepc  48607