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

This theorem is referenced by:  syl123anc  1386  syl213anc  1388  pythagtriplem18  16523  initoeu2  17721  psgnunilem1  19091  mulmarep1gsum1  21712  mulmarep1gsum2  21713  smadiadetlem4  21808  cramerimplem2  21823  cramerlem2  21827  cramer  21830  cnhaus  22495  dishaus  22523  ordthauslem  22524  pthaus  22779  txhaus  22788  xkohaus  22794  regr1lem  22880  methaus  23666  metnrmlem3  24014  iscgrad  27162  f1otrge  27223  axpaschlem  27298  wwlksnwwlksnon  28268  n4cyclfrgr  28643  br8d  30938  lt2addrd  31062  xlt2addrd  31069  br8  33711  br4  33713  nosupres  33898  nosupbnd1lem1  33899  nosupbnd2  33907  noinfres  33913  noinfbnd1lem1  33914  btwnxfr  34346  lineext  34366  brsegle  34398  brsegle2  34399  lfl0  37067  lfladd  37068  lflsub  37069  lflmul  37070  lflnegcl  37077  lflvscl  37079  lkrlss  37097  3dimlem3  37463  3dimlem4  37466  3dim3  37471  2llnm3N  37571  2lplnja  37621  4atex  38078  4atex3  38083  trlval4  38190  cdleme7c  38247  cdleme7d  38248  cdleme7ga  38250  cdleme21h  38336  cdleme21i  38337  cdleme21j  38338  cdleme21  38339  cdleme32d  38446  cdleme32f  38448  cdleme35h2  38459  cdleme38m  38465  cdleme40m  38469  cdlemg8  38633  cdlemg11a  38639  cdlemg10a  38642  cdlemg12b  38646  cdlemg12d  38648  cdlemg12f  38650  cdlemg12g  38651  cdlemg15a  38657  cdlemg16  38659  cdlemg16z  38661  cdlemg18a  38680  cdlemg24  38690  cdlemg29  38707  cdlemg33b  38709  cdlemg38  38717  cdlemg39  38718  cdlemg40  38719  cdlemg44b  38734  cdlemj2  38824  cdlemk7  38850  cdlemk12  38852  cdlemk12u  38874  cdlemk32  38899  cdlemk25-3  38906  cdlemk34  38912  cdlemkid3N  38935  cdlemkid4  38936  cdlemk11t  38948  cdlemk53  38959  cdlemk55b  38962  cdleml3N  38980  hdmapln1  39908  sepfsepc  46182