Theorem syl131anc 1385

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 1128	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃 ∧ 𝜏))
6		syl23anc.5	. 2 ⊢ (𝜑 → 𝜂)
7		syl131anc.6	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁)
8	1, 5, 6, 7	syl3anc 1373	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 207  df-an 396  df-3an 1088

This theorem is referenced by:  syl132anc  1390  syl231anc  1392  syl133anc  1395  initoeu2lem1  17918  estrres  18042  mulgdir  19016  omndadd2d  20040  omndadd2rd  20041  submomnd  20042  omndmul2  20043  omndmul3  20044  ogrpinv0le  20046  ogrpsub  20047  ogrpaddltbi  20049  ogrpaddltrd  20050  ogrpinv0lt  20053  orngsqr  20779  ornglmulle  20780  orngrmulle  20781  ofldchr  21511  umgr2edg  29185  2pthfrgr  30259  isarchi3  33151  archirngz  33153  archiabllem1a  33155  archiabllem1b  33156  archiabllem2a  33158  archiabllem2c  33159  lineext  36109  brsegle2  36142  cvrcmp  39321  cvrcmp2  39322  atcvreq0  39352  cvlatexch3  39376  cvlcvr1  39377  cvlsupr2  39381  cvlsupr7  39386  atnlej1  39417  atnlej2  39418  cvrval3  39451  ltltncvr  39461  atcvrneN  39468  atcvrj2b  39470  atbtwnex  39486  3noncolr2  39487  3noncolr1N  39488  4noncolr3  39491  3dimlem2  39497  3dimlem3a  39498  3dimlem3  39499  3dimlem3OLDN  39500  3dimlem4a  39501  3dimlem4  39502  3dimlem4OLDN  39503  ps-1  39515  hlatexch4  39519  3atlem1  39521  3atlem2  39522  3atlem3  39523  3atlem4  39524  3atlem5  39525  3atlem6  39526  3atlem7  39527  2llnmat  39562  ps-2c  39566  lplnri3N  39593  lplnexllnN  39602  2llnmeqat  39609  4atlem0a  39631  4atlem0ae  39632  4atlem0be  39633  4atlem9  39641  4atlem10a  39642  4atlem10b  39643  4atlem10  39644  4atlem11a  39645  4atlem11  39647  4atlem12a  39648  dalemcnes  39688  dalempnes  39689  dalemqnet  39690  dalem1  39697  dalemdea  39700  dalem3  39702  dalem5  39705  dalem-cly  39709  dalem27  39737  dalem28  39738  dalem41  39751  dalem45  39755  dalem48  39758  lneq2at  39816  2lnat  39822  2llnma1  39825  2llnma3r  39826  2llnma2  39827  cdlemblem  39831  paddasslem2  39859  pmodl42N  39889  hlmod1i  39894  atmod1i1m  39896  atmod2i1  39899  atmod2i2  39900  atmod3i1  39902  llnexchb2lem  39906  dalawlem2  39910  dalawlem3  39911  dalawlem6  39914  dalawlem7  39915  dalawlem11  39919  dalawlem12  39920  pexmidlem3N  40010  lhpexle3lem  40049  lhpmcvr3  40063  lhp2at0  40070  lhpelim  40075  lhpmod2i2  40076  lhpmod6i1  40077  4atexlempns  40100  4atexlemunv  40104  4atexlemc  40107  4atexlemnclw  40108  4atexlemex2  40109  4atexlemex6  40112  4atex  40114  4atex3  40119  trljat1  40204  trljat2  40205  ltrnatlw  40221  trlval4  40226  cdlemc1  40229  cdlemc3  40231  cdlemc6  40234  cdlemd3  40238  cdlemd4  40239  cdlemd5  40240  cdlemd6  40241  cdlemd7  40242  cdleme00a  40247  cdleme0cp  40252  cdleme0cq  40253  cdleme0e  40255  cdleme02N  40260  cdleme0ex2N  40262  cdleme0moN  40263  cdleme1  40265  cdleme2  40266  cdleme3e  40270  cdleme3g  40272  cdleme3h  40273  cdleme4  40276  cdleme5  40278  cdleme7aa  40280  cdleme7c  40283  cdleme7d  40284  cdleme7e  40285  cdleme8  40288  cdleme9  40291  cdleme10  40292  cdleme16aN  40297  cdleme11a  40298  cdleme11c  40299  cdleme11dN  40300  cdleme11e  40301  cdleme11g  40303  cdleme11h  40304  cdleme11j  40305  cdleme11k  40306  cdleme12  40309  cdleme15a  40312  cdleme15b  40313  cdleme16b  40317  cdleme17c  40326  cdleme0nex  40328  cdleme18d  40333  cdlemednpq  40337  cdleme20zN  40339  cdleme20y  40340  cdleme19a  40341  cdleme19d  40344  cdleme20aN  40347  cdleme20c  40349  cdleme20i  40355  cdleme20j  40356  cdleme21a  40363  cdleme21b  40364  cdleme21c  40365  cdleme21ct  40367  cdleme22cN  40380  cdleme22d  40381  cdleme22e  40382  cdleme22eALTN  40383  cdleme22f  40384  cdleme22f2  40385  cdleme22g  40386  cdleme23c  40389  cdleme41sn3a  40471  cdleme32le  40485  cdleme35b  40488  cdleme35c  40489  cdleme35d  40490  cdleme35e  40491  cdleme36a  40498  cdleme37m  40500  cdleme39a  40503  cdleme42a  40509  cdleme17d2  40533  cdlemeg46frv  40563  cdlemeg46rgv  40566  cdlemf1  40599  cdlemg2fv2  40638  cdlemg2l  40641  cdlemg2m  40642  cdlemg4d  40651  cdlemg4e  40652  cdlemg4f  40653  cdlemg4  40655  cdlemg6c  40658  cdlemg9a  40670  cdlemg10bALTN  40674  cdlemg12a  40681  cdlemg13  40690  cdlemg14f  40691  cdlemg14g  40692  cdlemg17i  40707  cdlemg17pq  40710  cdlemg19  40722  cdlemg21  40724  cdlemg27b  40734  cdlemg33c  40746  cdlemg33d  40747  trlcoabs2N  40760  cdlemg43  40768  cdlemg44b  40770  cdlemg44  40771  cdlemh1  40853  cdlemh2  40854  cdlemi1  40856  tendo0mul  40864  tendo0mulr  40865  cdlemk4  40872  cdlemk9  40877  cdlemk9bN  40878  cdlemk14  40892  cdlemkfid1N  40959  cdlemkid1  40960  cdlemk35s-id  40976  cdlemk39s-id  40978  cdlemk55a  40997  cdlemk55u  41004  cdlemk39u  41006  cdlemk19u  41008  cdlemk56  41009  cdleml8  41021  dia2dimlem1  41102  dia2dimlem2  41103  dia2dimlem3  41104  cdlemn10  41244  dihjust  41255  dihord1  41256  dihlsscpre  41272  dihvalcqpre  41273  dihglbcpreN  41338  dihmeetlem5  41346  dihmeetlem7N  41348  dihjatc1  41349  modmknepk  47392  modm2nep1  47396  modp2nep1  47397  modm1nep2  47398  modm1nem2  47399  lincreslvec3  48513  isldepslvec2  48516