Theorem syl131anc 1391

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
syl3anc.1	⊢ (𝜑 → 𝜓)
syl3anc.2	⊢ (𝜑 → 𝜒)
syl3anc.3	⊢ (𝜑 → 𝜃)
syl3Xanc.4	⊢ (𝜑 → 𝜏)
syl23anc.5	⊢ (𝜑 → 𝜂)
syl131anc.6	⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁)

Assertion

Ref	Expression
syl131anc	⊢ (𝜑 → 𝜁)

Proof of Theorem syl131anc

Step	Hyp	Ref	Expression
1		syl3anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl3anc.2	. . 3 ⊢ (𝜑 → 𝜒)
3		syl3anc.3	. . 3 ⊢ (𝜑 → 𝜃)
4		syl3Xanc.4	. . 3 ⊢ (𝜑 → 𝜏)
5	2, 3, 4	3jca 1134	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃 ∧ 𝜏))
6		syl23anc.5	. 2 ⊢ (𝜑 → 𝜂)
7		syl131anc.6	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁)
8	1, 5, 6, 7	syl3anc 1379	1 ⊢ (𝜑 → 𝜁)

Syntax hints:   → wi 4   ∧ w3a 1092

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

This theorem is referenced by:  syl132anc  1396  syl231anc  1398  syl133anc  1401  initoeu2lem1  17979  estrres  18103  mulgdir  19080  omndadd2d  20103  omndadd2rd  20104  submomnd  20105  omndmul2  20106  omndmul3  20107  ogrpinv0le  20109  ogrpsub  20110  ogrpaddltbi  20112  ogrpaddltrd  20113  ogrpinv0lt  20116  orngsqr  20845  ornglmulle  20846  orngrmulle  20847  ofldchr  21558  umgr2edg  29303  2pthfrgr  30379  isarchi3  33275  archirngz  33277  archiabllem1a  33279  archiabllem1b  33280  archiabllem2a  33282  archiabllem2c  33283  lineext  36311  brsegle2  36344  cvrcmp  39782  cvrcmp2  39783  atcvreq0  39813  cvlatexch3  39837  cvlcvr1  39838  cvlsupr2  39842  cvlsupr7  39847  atnlej1  39878  atnlej2  39879  cvrval3  39912  ltltncvr  39922  atcvrneN  39929  atcvrj2b  39931  atbtwnex  39947  3noncolr2  39948  3noncolr1N  39949  4noncolr3  39952  3dimlem2  39958  3dimlem3a  39959  3dimlem3  39960  3dimlem3OLDN  39961  3dimlem4a  39962  3dimlem4  39963  3dimlem4OLDN  39964  ps-1  39976  hlatexch4  39980  3atlem1  39982  3atlem2  39983  3atlem3  39984  3atlem4  39985  3atlem5  39986  3atlem6  39987  3atlem7  39988  2llnmat  40023  ps-2c  40027  lplnri3N  40054  lplnexllnN  40063  2llnmeqat  40070  4atlem0a  40092  4atlem0ae  40093  4atlem0be  40094  4atlem9  40102  4atlem10a  40103  4atlem10b  40104  4atlem10  40105  4atlem11a  40106  4atlem11  40108  4atlem12a  40109  dalemcnes  40149  dalempnes  40150  dalemqnet  40151  dalem1  40158  dalemdea  40161  dalem3  40163  dalem5  40166  dalem-cly  40170  dalem27  40198  dalem28  40199  dalem41  40212  dalem45  40216  dalem48  40219  lneq2at  40277  2lnat  40283  2llnma1  40286  2llnma3r  40287  2llnma2  40288  cdlemblem  40292  paddasslem2  40320  pmodl42N  40350  hlmod1i  40355  atmod1i1m  40357  atmod2i1  40360  atmod2i2  40361  atmod3i1  40363  llnexchb2lem  40367  dalawlem2  40371  dalawlem3  40372  dalawlem6  40375  dalawlem7  40376  dalawlem11  40380  dalawlem12  40381  pexmidlem3N  40471  lhpexle3lem  40510  lhpmcvr3  40524  lhp2at0  40531  lhpelim  40536  lhpmod2i2  40537  lhpmod6i1  40538  4atexlempns  40561  4atexlemunv  40565  4atexlemc  40568  4atexlemnclw  40569  4atexlemex2  40570  4atexlemex6  40573  4atex  40575  4atex3  40580  trljat1  40665  trljat2  40666  ltrnatlw  40682  trlval4  40687  cdlemc1  40690  cdlemc3  40692  cdlemc6  40695  cdlemd3  40699  cdlemd4  40700  cdlemd5  40701  cdlemd6  40702  cdlemd7  40703  cdleme00a  40708  cdleme0cp  40713  cdleme0cq  40714  cdleme0e  40716  cdleme02N  40721  cdleme0ex2N  40723  cdleme0moN  40724  cdleme1  40726  cdleme2  40727  cdleme3e  40731  cdleme3g  40733  cdleme3h  40734  cdleme4  40737  cdleme5  40739  cdleme7aa  40741  cdleme7c  40744  cdleme7d  40745  cdleme7e  40746  cdleme8  40749  cdleme9  40752  cdleme10  40753  cdleme16aN  40758  cdleme11a  40759  cdleme11c  40760  cdleme11dN  40761  cdleme11e  40762  cdleme11g  40764  cdleme11h  40765  cdleme11j  40766  cdleme11k  40767  cdleme12  40770  cdleme15a  40773  cdleme15b  40774  cdleme16b  40778  cdleme17c  40787  cdleme0nex  40789  cdleme18d  40794  cdlemednpq  40798  cdleme20zN  40800  cdleme20y  40801  cdleme19a  40802  cdleme19d  40805  cdleme20aN  40808  cdleme20c  40810  cdleme20i  40816  cdleme20j  40817  cdleme21a  40824  cdleme21b  40825  cdleme21c  40826  cdleme21ct  40828  cdleme22cN  40841  cdleme22d  40842  cdleme22e  40843  cdleme22eALTN  40844  cdleme22f  40845  cdleme22f2  40846  cdleme22g  40847  cdleme23c  40850  cdleme41sn3a  40932  cdleme32le  40946  cdleme35b  40949  cdleme35c  40950  cdleme35d  40951  cdleme35e  40952  cdleme36a  40959  cdleme37m  40961  cdleme39a  40964  cdleme42a  40970  cdleme17d2  40994  cdlemeg46frv  41024  cdlemeg46rgv  41027  cdlemf1  41060  cdlemg2fv2  41099  cdlemg2l  41102  cdlemg2m  41103  cdlemg4d  41112  cdlemg4e  41113  cdlemg4f  41114  cdlemg4  41116  cdlemg6c  41119  cdlemg9a  41131  cdlemg10bALTN  41135  cdlemg12a  41142  cdlemg13  41151  cdlemg14f  41152  cdlemg14g  41153  cdlemg17i  41168  cdlemg17pq  41171  cdlemg19  41183  cdlemg21  41185  cdlemg27b  41195  cdlemg33c  41207  cdlemg33d  41208  trlcoabs2N  41221  cdlemg43  41229  cdlemg44b  41231  cdlemg44  41232  cdlemh1  41314  cdlemh2  41315  cdlemi1  41317  tendo0mul  41325  tendo0mulr  41326  cdlemk4  41333  cdlemk9  41338  cdlemk9bN  41339  cdlemk14  41353  cdlemkfid1N  41420  cdlemkid1  41421  cdlemk35s-id  41437  cdlemk39s-id  41439  cdlemk55a  41458  cdlemk55u  41465  cdlemk39u  41467  cdlemk19u  41469  cdlemk56  41470  cdleml8  41482  dia2dimlem1  41563  dia2dimlem2  41564  dia2dimlem3  41565  cdlemn10  41705  dihjust  41716  dihord1  41717  dihlsscpre  41733  dihvalcqpre  41734  dihglbcpreN  41799  dihmeetlem5  41807  dihmeetlem7N  41809  dihjatc1  41810  modmknepk  47838  modm2nep1  47842  modp2nep1  47843  modm1nep2  47844  modm1nem2  47845  lincreslvec3  48980  isldepslvec2  48983