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  17913  estrres  18037  mulgdir  19011  omndadd2d  20035  omndadd2rd  20036  submomnd  20037  omndmul2  20038  omndmul3  20039  ogrpinv0le  20041  ogrpsub  20042  ogrpaddltbi  20044  ogrpaddltrd  20045  ogrpinv0lt  20048  orngsqr  20774  ornglmulle  20775  orngrmulle  20776  ofldchr  21506  umgr2edg  29180  2pthfrgr  30254  isarchi3  33146  archirngz  33148  archiabllem1a  33150  archiabllem1b  33151  archiabllem2a  33153  archiabllem2c  33154  lineext  36089  brsegle2  36122  cvrcmp  39301  cvrcmp2  39302  atcvreq0  39332  cvlatexch3  39356  cvlcvr1  39357  cvlsupr2  39361  cvlsupr7  39366  atnlej1  39397  atnlej2  39398  cvrval3  39431  ltltncvr  39441  atcvrneN  39448  atcvrj2b  39450  atbtwnex  39466  3noncolr2  39467  3noncolr1N  39468  4noncolr3  39471  3dimlem2  39477  3dimlem3a  39478  3dimlem3  39479  3dimlem3OLDN  39480  3dimlem4a  39481  3dimlem4  39482  3dimlem4OLDN  39483  ps-1  39495  hlatexch4  39499  3atlem1  39501  3atlem2  39502  3atlem3  39503  3atlem4  39504  3atlem5  39505  3atlem6  39506  3atlem7  39507  2llnmat  39542  ps-2c  39546  lplnri3N  39573  lplnexllnN  39582  2llnmeqat  39589  4atlem0a  39611  4atlem0ae  39612  4atlem0be  39613  4atlem9  39621  4atlem10a  39622  4atlem10b  39623  4atlem10  39624  4atlem11a  39625  4atlem11  39627  4atlem12a  39628  dalemcnes  39668  dalempnes  39669  dalemqnet  39670  dalem1  39677  dalemdea  39680  dalem3  39682  dalem5  39685  dalem-cly  39689  dalem27  39717  dalem28  39718  dalem41  39731  dalem45  39735  dalem48  39738  lneq2at  39796  2lnat  39802  2llnma1  39805  2llnma3r  39806  2llnma2  39807  cdlemblem  39811  paddasslem2  39839  pmodl42N  39869  hlmod1i  39874  atmod1i1m  39876  atmod2i1  39879  atmod2i2  39880  atmod3i1  39882  llnexchb2lem  39886  dalawlem2  39890  dalawlem3  39891  dalawlem6  39894  dalawlem7  39895  dalawlem11  39899  dalawlem12  39900  pexmidlem3N  39990  lhpexle3lem  40029  lhpmcvr3  40043  lhp2at0  40050  lhpelim  40055  lhpmod2i2  40056  lhpmod6i1  40057  4atexlempns  40080  4atexlemunv  40084  4atexlemc  40087  4atexlemnclw  40088  4atexlemex2  40089  4atexlemex6  40092  4atex  40094  4atex3  40099  trljat1  40184  trljat2  40185  ltrnatlw  40201  trlval4  40206  cdlemc1  40209  cdlemc3  40211  cdlemc6  40214  cdlemd3  40218  cdlemd4  40219  cdlemd5  40220  cdlemd6  40221  cdlemd7  40222  cdleme00a  40227  cdleme0cp  40232  cdleme0cq  40233  cdleme0e  40235  cdleme02N  40240  cdleme0ex2N  40242  cdleme0moN  40243  cdleme1  40245  cdleme2  40246  cdleme3e  40250  cdleme3g  40252  cdleme3h  40253  cdleme4  40256  cdleme5  40258  cdleme7aa  40260  cdleme7c  40263  cdleme7d  40264  cdleme7e  40265  cdleme8  40268  cdleme9  40271  cdleme10  40272  cdleme16aN  40277  cdleme11a  40278  cdleme11c  40279  cdleme11dN  40280  cdleme11e  40281  cdleme11g  40283  cdleme11h  40284  cdleme11j  40285  cdleme11k  40286  cdleme12  40289  cdleme15a  40292  cdleme15b  40293  cdleme16b  40297  cdleme17c  40306  cdleme0nex  40308  cdleme18d  40313  cdlemednpq  40317  cdleme20zN  40319  cdleme20y  40320  cdleme19a  40321  cdleme19d  40324  cdleme20aN  40327  cdleme20c  40329  cdleme20i  40335  cdleme20j  40336  cdleme21a  40343  cdleme21b  40344  cdleme21c  40345  cdleme21ct  40347  cdleme22cN  40360  cdleme22d  40361  cdleme22e  40362  cdleme22eALTN  40363  cdleme22f  40364  cdleme22f2  40365  cdleme22g  40366  cdleme23c  40369  cdleme41sn3a  40451  cdleme32le  40465  cdleme35b  40468  cdleme35c  40469  cdleme35d  40470  cdleme35e  40471  cdleme36a  40478  cdleme37m  40480  cdleme39a  40483  cdleme42a  40489  cdleme17d2  40513  cdlemeg46frv  40543  cdlemeg46rgv  40546  cdlemf1  40579  cdlemg2fv2  40618  cdlemg2l  40621  cdlemg2m  40622  cdlemg4d  40631  cdlemg4e  40632  cdlemg4f  40633  cdlemg4  40635  cdlemg6c  40638  cdlemg9a  40650  cdlemg10bALTN  40654  cdlemg12a  40661  cdlemg13  40670  cdlemg14f  40671  cdlemg14g  40672  cdlemg17i  40687  cdlemg17pq  40690  cdlemg19  40702  cdlemg21  40704  cdlemg27b  40714  cdlemg33c  40726  cdlemg33d  40727  trlcoabs2N  40740  cdlemg43  40748  cdlemg44b  40750  cdlemg44  40751  cdlemh1  40833  cdlemh2  40834  cdlemi1  40836  tendo0mul  40844  tendo0mulr  40845  cdlemk4  40852  cdlemk9  40857  cdlemk9bN  40858  cdlemk14  40872  cdlemkfid1N  40939  cdlemkid1  40940  cdlemk35s-id  40956  cdlemk39s-id  40958  cdlemk55a  40977  cdlemk55u  40984  cdlemk39u  40986  cdlemk19u  40988  cdlemk56  40989  cdleml8  41001  dia2dimlem1  41082  dia2dimlem2  41083  dia2dimlem3  41084  cdlemn10  41224  dihjust  41235  dihord1  41236  dihlsscpre  41252  dihvalcqpre  41253  dihglbcpreN  41318  dihmeetlem5  41326  dihmeetlem7N  41328  dihjatc1  41329  modmknepk  47372  modm2nep1  47376  modp2nep1  47377  modm1nep2  47378  modm1nem2  47379  lincreslvec3  48493  isldepslvec2  48496