Theorem syl131anc 1331

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

Hypotheses

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

Assertion

Ref	Expression
syl131anc	⊢ (𝜑 → 𝜁)

Proof of Theorem syl131anc

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

Syntax hints:   → wi 4   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  syl132anc  1336  syl231anc  1338  syl133anc  1341  initoeu2lem1  16487  estrres  16602  mulgdir  17396  3v3e3cycl2  26192  omndadd2d  29039  omndadd2rd  29040  submomnd  29041  omndmul2  29043  omndmul3  29044  ogrpinvOLD  29046  ogrpinv0le  29047  ogrpsub  29048  ogrpaddltbi  29050  ogrpaddltrd  29051  ogrpinv0lt  29054  isarchi3  29072  archirngz  29074  archiabllem1a  29076  archiabllem1b  29077  archiabllem2a  29079  archiabllem2c  29080  orngsqr  29135  ornglmulle  29136  orngrmulle  29137  ofldchr  29145  lineext  31353  brsegle2  31386  cvrcmp  33588  cvrcmp2  33589  atcvreq0  33619  cvlatexch3  33643  cvlcvr1  33644  cvlsupr2  33648  cvlsupr7  33653  atnlej1  33683  atnlej2  33684  cvrval3  33717  ltltncvr  33727  atcvrneN  33734  atcvrj2b  33736  atbtwnex  33752  3noncolr2  33753  3noncolr1N  33754  4noncolr3  33757  3dimlem2  33763  3dimlem3a  33764  3dimlem3  33765  3dimlem3OLDN  33766  3dimlem4a  33767  3dimlem4  33768  3dimlem4OLDN  33769  ps-1  33781  hlatexch4  33785  3atlem1  33787  3atlem2  33788  3atlem3  33789  3atlem4  33790  3atlem5  33791  3atlem6  33792  3atlem7  33793  2llnmat  33828  ps-2c  33832  lplnri3N  33859  lplnexllnN  33868  2llnmeqat  33875  4atlem0a  33897  4atlem0ae  33898  4atlem0be  33899  4atlem9  33907  4atlem10a  33908  4atlem10b  33909  4atlem10  33910  4atlem11a  33911  4atlem11  33913  4atlem12a  33914  dalemcnes  33954  dalempnes  33955  dalemqnet  33956  dalem1  33963  dalemdea  33966  dalem3  33968  dalem5  33971  dalem-cly  33975  dalem27  34003  dalem28  34004  dalem41  34017  dalem45  34021  dalem48  34024  lneq2at  34082  2lnat  34088  2llnma1  34091  2llnma3r  34092  2llnma2  34093  cdlemblem  34097  paddasslem2  34125  pmodl42N  34155  hlmod1i  34160  atmod1i1m  34162  atmod2i1  34165  atmod2i2  34166  atmod3i1  34168  llnexchb2lem  34172  dalawlem2  34176  dalawlem3  34177  dalawlem6  34180  dalawlem7  34181  dalawlem11  34185  dalawlem12  34186  pexmidlem3N  34276  lhpexle3lem  34315  lhpmcvr3  34329  lhp2at0  34336  lhpelim  34341  lhpmod2i2  34342  lhpmod6i1  34343  4atexlempns  34366  4atexlemunv  34370  4atexlemc  34373  4atexlemnclw  34374  4atexlemex2  34375  4atexlemex6  34378  4atex  34380  4atex3  34385  trljat1  34471  trljat2  34472  ltrnatlw  34488  trlval4  34493  cdlemc1  34496  cdlemc3  34498  cdlemc6  34501  cdlemd3  34505  cdlemd4  34506  cdlemd5  34507  cdlemd6  34508  cdlemd7  34509  cdleme00a  34514  cdleme0cp  34519  cdleme0cq  34520  cdleme0e  34522  cdleme02N  34527  cdleme0ex2N  34529  cdleme0moN  34530  cdleme1  34532  cdleme2  34533  cdleme3e  34537  cdleme3g  34539  cdleme3h  34540  cdleme4  34543  cdleme5  34545  cdleme7aa  34547  cdleme7c  34550  cdleme7d  34551  cdleme7e  34552  cdleme8  34555  cdleme9  34558  cdleme10  34559  cdleme16aN  34564  cdleme11a  34565  cdleme11c  34566  cdleme11dN  34567  cdleme11e  34568  cdleme11g  34570  cdleme11h  34571  cdleme11j  34572  cdleme11k  34573  cdleme12  34576  cdleme15a  34579  cdleme15b  34580  cdleme16b  34584  cdleme17c  34593  cdleme0nex  34595  cdleme18d  34600  cdlemednpq  34604  cdleme20zN  34606  cdleme20y  34607  cdleme20yOLD  34608  cdleme19a  34609  cdleme19d  34612  cdleme20aN  34615  cdleme20c  34617  cdleme20i  34623  cdleme20j  34624  cdleme21a  34631  cdleme21b  34632  cdleme21c  34633  cdleme21ct  34635  cdleme22cN  34648  cdleme22d  34649  cdleme22e  34650  cdleme22eALTN  34651  cdleme22f  34652  cdleme22f2  34653  cdleme22g  34654  cdleme23c  34657  cdleme41sn3a  34739  cdleme32le  34753  cdleme35b  34756  cdleme35c  34757  cdleme35d  34758  cdleme35e  34759  cdleme36a  34766  cdleme37m  34768  cdleme39a  34771  cdleme42a  34777  cdleme17d2  34801  cdlemeg46frv  34831  cdlemeg46rgv  34834  cdlemf1  34867  cdlemg2fv2  34906  cdlemg2l  34909  cdlemg2m  34910  cdlemg4d  34919  cdlemg4e  34920  cdlemg4f  34921  cdlemg4  34923  cdlemg6c  34926  cdlemg9a  34938  cdlemg10bALTN  34942  cdlemg12a  34949  cdlemg13  34958  cdlemg14f  34959  cdlemg14g  34960  cdlemg17i  34975  cdlemg17pq  34978  cdlemg19  34990  cdlemg21  34992  cdlemg27b  35002  cdlemg33c  35014  cdlemg33d  35015  trlcoabs2N  35028  cdlemg43  35036  cdlemg44b  35038  cdlemg44  35039  cdlemh1  35121  cdlemh2  35122  cdlemi1  35124  tendo0mul  35132  tendo0mulr  35133  cdlemk4  35140  cdlemk9  35145  cdlemk9bN  35146  cdlemk14  35160  cdlemkfid1N  35227  cdlemkid1  35228  cdlemk35s-id  35244  cdlemk39s-id  35246  cdlemk55a  35265  cdlemk55u  35272  cdlemk39u  35274  cdlemk19u  35276  cdlemk56  35277  cdleml8  35289  dia2dimlem1  35371  dia2dimlem2  35372  dia2dimlem3  35373  cdlemn10  35513  dihjust  35524  dihord1  35525  dihlsscpre  35541  dihvalcqpre  35542  dihglbcpreN  35607  dihmeetlem5  35615  dihmeetlem7N  35617  dihjatc1  35618  2pthfrgr  41454  lincreslvec3  42065  isldepslvec2  42068