Theorem syl113anc 1380

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 1087

This theorem is referenced by:  syl123anc  1385  syl213anc  1387  pythagtriplem18  16461  initoeu2  17647  psgnunilem1  19016  mulmarep1gsum1  21630  mulmarep1gsum2  21631  smadiadetlem4  21726  cramerimplem2  21741  cramerlem2  21745  cramer  21748  cnhaus  22413  dishaus  22441  ordthauslem  22442  pthaus  22697  txhaus  22706  xkohaus  22712  regr1lem  22798  methaus  23582  metnrmlem3  23930  iscgrad  27076  f1otrge  27137  axpaschlem  27211  wwlksnwwlksnon  28181  n4cyclfrgr  28556  br8d  30851  lt2addrd  30976  xlt2addrd  30983  br8  33629  br4  33631  nosupres  33837  nosupbnd1lem1  33838  nosupbnd2  33846  noinfres  33852  noinfbnd1lem1  33853  btwnxfr  34285  lineext  34305  brsegle  34337  brsegle2  34338  lfl0  37006  lfladd  37007  lflsub  37008  lflmul  37009  lflnegcl  37016  lflvscl  37018  lkrlss  37036  3dimlem3  37402  3dimlem4  37405  3dim3  37410  2llnm3N  37510  2lplnja  37560  4atex  38017  4atex3  38022  trlval4  38129  cdleme7c  38186  cdleme7d  38187  cdleme7ga  38189  cdleme21h  38275  cdleme21i  38276  cdleme21j  38277  cdleme21  38278  cdleme32d  38385  cdleme32f  38387  cdleme35h2  38398  cdleme38m  38404  cdleme40m  38408  cdlemg8  38572  cdlemg11a  38578  cdlemg10a  38581  cdlemg12b  38585  cdlemg12d  38587  cdlemg12f  38589  cdlemg12g  38590  cdlemg15a  38596  cdlemg16  38598  cdlemg16z  38600  cdlemg18a  38619  cdlemg24  38629  cdlemg29  38646  cdlemg33b  38648  cdlemg38  38656  cdlemg39  38657  cdlemg40  38658  cdlemg44b  38673  cdlemj2  38763  cdlemk7  38789  cdlemk12  38791  cdlemk12u  38813  cdlemk32  38838  cdlemk25-3  38845  cdlemk34  38851  cdlemkid3N  38874  cdlemkid4  38875  cdlemk11t  38887  cdlemk53  38898  cdlemk55b  38901  cdleml3N  38919  hdmapln1  39847  sepfsepc  46109