Theorem syl131anc 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	⊢ (𝜑 → 𝜂)
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 1125	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃 ∧ 𝜏))
6		syl23anc.5	. 2 ⊢ (𝜑 → 𝜂)
7		syl131anc.6	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁)
8	1, 5, 6, 7	syl3anc 1368	1 ⊢ (𝜑 → 𝜁)

Syntax hints:   → wi 4   ∧ w3a 1084

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 395  df-3an 1086

This theorem is referenced by:  syl132anc  1385  syl231anc  1387  syl133anc  1390  initoeu2lem1  18011  estrres  18138  mulgdir  19074  umgr2edg  29099  2pthfrgr  30171  omndadd2d  32883  omndadd2rd  32884  submomnd  32885  omndmul2  32887  omndmul3  32888  ogrpinv0le  32890  ogrpsub  32891  ogrpaddltbi  32893  ogrpaddltrd  32894  ogrpinv0lt  32897  isarchi3  32992  archirngz  32994  archiabllem1a  32996  archiabllem1b  32997  archiabllem2a  32999  archiabllem2c  33000  orngsqr  33123  ornglmulle  33124  orngrmulle  33125  ofldchr  33133  lineext  35805  brsegle2  35838  cvrcmp  38887  cvrcmp2  38888  atcvreq0  38918  cvlatexch3  38942  cvlcvr1  38943  cvlsupr2  38947  cvlsupr7  38952  atnlej1  38984  atnlej2  38985  cvrval3  39018  ltltncvr  39028  atcvrneN  39035  atcvrj2b  39037  atbtwnex  39053  3noncolr2  39054  3noncolr1N  39055  4noncolr3  39058  3dimlem2  39064  3dimlem3a  39065  3dimlem3  39066  3dimlem3OLDN  39067  3dimlem4a  39068  3dimlem4  39069  3dimlem4OLDN  39070  ps-1  39082  hlatexch4  39086  3atlem1  39088  3atlem2  39089  3atlem3  39090  3atlem4  39091  3atlem5  39092  3atlem6  39093  3atlem7  39094  2llnmat  39129  ps-2c  39133  lplnri3N  39160  lplnexllnN  39169  2llnmeqat  39176  4atlem0a  39198  4atlem0ae  39199  4atlem0be  39200  4atlem9  39208  4atlem10a  39209  4atlem10b  39210  4atlem10  39211  4atlem11a  39212  4atlem11  39214  4atlem12a  39215  dalemcnes  39255  dalempnes  39256  dalemqnet  39257  dalem1  39264  dalemdea  39267  dalem3  39269  dalem5  39272  dalem-cly  39276  dalem27  39304  dalem28  39305  dalem41  39318  dalem45  39322  dalem48  39325  lneq2at  39383  2lnat  39389  2llnma1  39392  2llnma3r  39393  2llnma2  39394  cdlemblem  39398  paddasslem2  39426  pmodl42N  39456  hlmod1i  39461  atmod1i1m  39463  atmod2i1  39466  atmod2i2  39467  atmod3i1  39469  llnexchb2lem  39473  dalawlem2  39477  dalawlem3  39478  dalawlem6  39481  dalawlem7  39482  dalawlem11  39486  dalawlem12  39487  pexmidlem3N  39577  lhpexle3lem  39616  lhpmcvr3  39630  lhp2at0  39637  lhpelim  39642  lhpmod2i2  39643  lhpmod6i1  39644  4atexlempns  39667  4atexlemunv  39671  4atexlemc  39674  4atexlemnclw  39675  4atexlemex2  39676  4atexlemex6  39679  4atex  39681  4atex3  39686  trljat1  39771  trljat2  39772  ltrnatlw  39788  trlval4  39793  cdlemc1  39796  cdlemc3  39798  cdlemc6  39801  cdlemd3  39805  cdlemd4  39806  cdlemd5  39807  cdlemd6  39808  cdlemd7  39809  cdleme00a  39814  cdleme0cp  39819  cdleme0cq  39820  cdleme0e  39822  cdleme02N  39827  cdleme0ex2N  39829  cdleme0moN  39830  cdleme1  39832  cdleme2  39833  cdleme3e  39837  cdleme3g  39839  cdleme3h  39840  cdleme4  39843  cdleme5  39845  cdleme7aa  39847  cdleme7c  39850  cdleme7d  39851  cdleme7e  39852  cdleme8  39855  cdleme9  39858  cdleme10  39859  cdleme16aN  39864  cdleme11a  39865  cdleme11c  39866  cdleme11dN  39867  cdleme11e  39868  cdleme11g  39870  cdleme11h  39871  cdleme11j  39872  cdleme11k  39873  cdleme12  39876  cdleme15a  39879  cdleme15b  39880  cdleme16b  39884  cdleme17c  39893  cdleme0nex  39895  cdleme18d  39900  cdlemednpq  39904  cdleme20zN  39906  cdleme20y  39907  cdleme19a  39908  cdleme19d  39911  cdleme20aN  39914  cdleme20c  39916  cdleme20i  39922  cdleme20j  39923  cdleme21a  39930  cdleme21b  39931  cdleme21c  39932  cdleme21ct  39934  cdleme22cN  39947  cdleme22d  39948  cdleme22e  39949  cdleme22eALTN  39950  cdleme22f  39951  cdleme22f2  39952  cdleme22g  39953  cdleme23c  39956  cdleme41sn3a  40038  cdleme32le  40052  cdleme35b  40055  cdleme35c  40056  cdleme35d  40057  cdleme35e  40058  cdleme36a  40065  cdleme37m  40067  cdleme39a  40070  cdleme42a  40076  cdleme17d2  40100  cdlemeg46frv  40130  cdlemeg46rgv  40133  cdlemf1  40166  cdlemg2fv2  40205  cdlemg2l  40208  cdlemg2m  40209  cdlemg4d  40218  cdlemg4e  40219  cdlemg4f  40220  cdlemg4  40222  cdlemg6c  40225  cdlemg9a  40237  cdlemg10bALTN  40241  cdlemg12a  40248  cdlemg13  40257  cdlemg14f  40258  cdlemg14g  40259  cdlemg17i  40274  cdlemg17pq  40277  cdlemg19  40289  cdlemg21  40291  cdlemg27b  40301  cdlemg33c  40313  cdlemg33d  40314  trlcoabs2N  40327  cdlemg43  40335  cdlemg44b  40337  cdlemg44  40338  cdlemh1  40420  cdlemh2  40421  cdlemi1  40423  tendo0mul  40431  tendo0mulr  40432  cdlemk4  40439  cdlemk9  40444  cdlemk9bN  40445  cdlemk14  40459  cdlemkfid1N  40526  cdlemkid1  40527  cdlemk35s-id  40543  cdlemk39s-id  40545  cdlemk55a  40564  cdlemk55u  40571  cdlemk39u  40573  cdlemk19u  40575  cdlemk56  40576  cdleml8  40588  dia2dimlem1  40669  dia2dimlem2  40670  dia2dimlem3  40671  cdlemn10  40811  dihjust  40822  dihord1  40823  dihlsscpre  40839  dihvalcqpre  40840  dihglbcpreN  40905  dihmeetlem5  40913  dihmeetlem7N  40915  dihjatc1  40916  lincreslvec3  47738  isldepslvec2  47741