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  17939  estrres  18063  mulgdir  19003  omndadd2d  20027  omndadd2rd  20028  submomnd  20029  omndmul2  20030  omndmul3  20031  ogrpinv0le  20033  ogrpsub  20034  ogrpaddltbi  20036  ogrpaddltrd  20037  ogrpinv0lt  20040  orngsqr  20769  ornglmulle  20770  orngrmulle  20771  ofldchr  21501  umgr2edg  29172  2pthfrgr  30246  isarchi3  33139  archirngz  33141  archiabllem1a  33143  archiabllem1b  33144  archiabllem2a  33146  archiabllem2c  33147  lineext  36049  brsegle2  36082  cvrcmp  39261  cvrcmp2  39262  atcvreq0  39292  cvlatexch3  39316  cvlcvr1  39317  cvlsupr2  39321  cvlsupr7  39326  atnlej1  39358  atnlej2  39359  cvrval3  39392  ltltncvr  39402  atcvrneN  39409  atcvrj2b  39411  atbtwnex  39427  3noncolr2  39428  3noncolr1N  39429  4noncolr3  39432  3dimlem2  39438  3dimlem3a  39439  3dimlem3  39440  3dimlem3OLDN  39441  3dimlem4a  39442  3dimlem4  39443  3dimlem4OLDN  39444  ps-1  39456  hlatexch4  39460  3atlem1  39462  3atlem2  39463  3atlem3  39464  3atlem4  39465  3atlem5  39466  3atlem6  39467  3atlem7  39468  2llnmat  39503  ps-2c  39507  lplnri3N  39534  lplnexllnN  39543  2llnmeqat  39550  4atlem0a  39572  4atlem0ae  39573  4atlem0be  39574  4atlem9  39582  4atlem10a  39583  4atlem10b  39584  4atlem10  39585  4atlem11a  39586  4atlem11  39588  4atlem12a  39589  dalemcnes  39629  dalempnes  39630  dalemqnet  39631  dalem1  39638  dalemdea  39641  dalem3  39643  dalem5  39646  dalem-cly  39650  dalem27  39678  dalem28  39679  dalem41  39692  dalem45  39696  dalem48  39699  lneq2at  39757  2lnat  39763  2llnma1  39766  2llnma3r  39767  2llnma2  39768  cdlemblem  39772  paddasslem2  39800  pmodl42N  39830  hlmod1i  39835  atmod1i1m  39837  atmod2i1  39840  atmod2i2  39841  atmod3i1  39843  llnexchb2lem  39847  dalawlem2  39851  dalawlem3  39852  dalawlem6  39855  dalawlem7  39856  dalawlem11  39860  dalawlem12  39861  pexmidlem3N  39951  lhpexle3lem  39990  lhpmcvr3  40004  lhp2at0  40011  lhpelim  40016  lhpmod2i2  40017  lhpmod6i1  40018  4atexlempns  40041  4atexlemunv  40045  4atexlemc  40048  4atexlemnclw  40049  4atexlemex2  40050  4atexlemex6  40053  4atex  40055  4atex3  40060  trljat1  40145  trljat2  40146  ltrnatlw  40162  trlval4  40167  cdlemc1  40170  cdlemc3  40172  cdlemc6  40175  cdlemd3  40179  cdlemd4  40180  cdlemd5  40181  cdlemd6  40182  cdlemd7  40183  cdleme00a  40188  cdleme0cp  40193  cdleme0cq  40194  cdleme0e  40196  cdleme02N  40201  cdleme0ex2N  40203  cdleme0moN  40204  cdleme1  40206  cdleme2  40207  cdleme3e  40211  cdleme3g  40213  cdleme3h  40214  cdleme4  40217  cdleme5  40219  cdleme7aa  40221  cdleme7c  40224  cdleme7d  40225  cdleme7e  40226  cdleme8  40229  cdleme9  40232  cdleme10  40233  cdleme16aN  40238  cdleme11a  40239  cdleme11c  40240  cdleme11dN  40241  cdleme11e  40242  cdleme11g  40244  cdleme11h  40245  cdleme11j  40246  cdleme11k  40247  cdleme12  40250  cdleme15a  40253  cdleme15b  40254  cdleme16b  40258  cdleme17c  40267  cdleme0nex  40269  cdleme18d  40274  cdlemednpq  40278  cdleme20zN  40280  cdleme20y  40281  cdleme19a  40282  cdleme19d  40285  cdleme20aN  40288  cdleme20c  40290  cdleme20i  40296  cdleme20j  40297  cdleme21a  40304  cdleme21b  40305  cdleme21c  40306  cdleme21ct  40308  cdleme22cN  40321  cdleme22d  40322  cdleme22e  40323  cdleme22eALTN  40324  cdleme22f  40325  cdleme22f2  40326  cdleme22g  40327  cdleme23c  40330  cdleme41sn3a  40412  cdleme32le  40426  cdleme35b  40429  cdleme35c  40430  cdleme35d  40431  cdleme35e  40432  cdleme36a  40439  cdleme37m  40441  cdleme39a  40444  cdleme42a  40450  cdleme17d2  40474  cdlemeg46frv  40504  cdlemeg46rgv  40507  cdlemf1  40540  cdlemg2fv2  40579  cdlemg2l  40582  cdlemg2m  40583  cdlemg4d  40592  cdlemg4e  40593  cdlemg4f  40594  cdlemg4  40596  cdlemg6c  40599  cdlemg9a  40611  cdlemg10bALTN  40615  cdlemg12a  40622  cdlemg13  40631  cdlemg14f  40632  cdlemg14g  40633  cdlemg17i  40648  cdlemg17pq  40651  cdlemg19  40663  cdlemg21  40665  cdlemg27b  40675  cdlemg33c  40687  cdlemg33d  40688  trlcoabs2N  40701  cdlemg43  40709  cdlemg44b  40711  cdlemg44  40712  cdlemh1  40794  cdlemh2  40795  cdlemi1  40797  tendo0mul  40805  tendo0mulr  40806  cdlemk4  40813  cdlemk9  40818  cdlemk9bN  40819  cdlemk14  40833  cdlemkfid1N  40900  cdlemkid1  40901  cdlemk35s-id  40917  cdlemk39s-id  40919  cdlemk55a  40938  cdlemk55u  40945  cdlemk39u  40947  cdlemk19u  40949  cdlemk56  40950  cdleml8  40962  dia2dimlem1  41043  dia2dimlem2  41044  dia2dimlem3  41045  cdlemn10  41185  dihjust  41196  dihord1  41197  dihlsscpre  41213  dihvalcqpre  41214  dihglbcpreN  41279  dihmeetlem5  41287  dihmeetlem7N  41289  dihjatc1  41290  modmknepk  47347  modm2nep1  47351  modp2nep1  47352  modm1nep2  47353  modm1nem2  47354  lincreslvec3  48468  isldepslvec2  48471