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  18025  estrres  18149  mulgdir  19087  umgr2edg  29134  2pthfrgr  30211  omndadd2d  33022  omndadd2rd  33023  submomnd  33024  omndmul2  33026  omndmul3  33027  ogrpinv0le  33029  ogrpsub  33030  ogrpaddltbi  33032  ogrpaddltrd  33033  ogrpinv0lt  33036  isarchi3  33131  archirngz  33133  archiabllem1a  33135  archiabllem1b  33136  archiabllem2a  33138  archiabllem2c  33139  orngsqr  33272  ornglmulle  33273  orngrmulle  33274  ofldchr  33282  lineext  36040  brsegle2  36073  cvrcmp  39247  cvrcmp2  39248  atcvreq0  39278  cvlatexch3  39302  cvlcvr1  39303  cvlsupr2  39307  cvlsupr7  39312  atnlej1  39344  atnlej2  39345  cvrval3  39378  ltltncvr  39388  atcvrneN  39395  atcvrj2b  39397  atbtwnex  39413  3noncolr2  39414  3noncolr1N  39415  4noncolr3  39418  3dimlem2  39424  3dimlem3a  39425  3dimlem3  39426  3dimlem3OLDN  39427  3dimlem4a  39428  3dimlem4  39429  3dimlem4OLDN  39430  ps-1  39442  hlatexch4  39446  3atlem1  39448  3atlem2  39449  3atlem3  39450  3atlem4  39451  3atlem5  39452  3atlem6  39453  3atlem7  39454  2llnmat  39489  ps-2c  39493  lplnri3N  39520  lplnexllnN  39529  2llnmeqat  39536  4atlem0a  39558  4atlem0ae  39559  4atlem0be  39560  4atlem9  39568  4atlem10a  39569  4atlem10b  39570  4atlem10  39571  4atlem11a  39572  4atlem11  39574  4atlem12a  39575  dalemcnes  39615  dalempnes  39616  dalemqnet  39617  dalem1  39624  dalemdea  39627  dalem3  39629  dalem5  39632  dalem-cly  39636  dalem27  39664  dalem28  39665  dalem41  39678  dalem45  39682  dalem48  39685  lneq2at  39743  2lnat  39749  2llnma1  39752  2llnma3r  39753  2llnma2  39754  cdlemblem  39758  paddasslem2  39786  pmodl42N  39816  hlmod1i  39821  atmod1i1m  39823  atmod2i1  39826  atmod2i2  39827  atmod3i1  39829  llnexchb2lem  39833  dalawlem2  39837  dalawlem3  39838  dalawlem6  39841  dalawlem7  39842  dalawlem11  39846  dalawlem12  39847  pexmidlem3N  39937  lhpexle3lem  39976  lhpmcvr3  39990  lhp2at0  39997  lhpelim  40002  lhpmod2i2  40003  lhpmod6i1  40004  4atexlempns  40027  4atexlemunv  40031  4atexlemc  40034  4atexlemnclw  40035  4atexlemex2  40036  4atexlemex6  40039  4atex  40041  4atex3  40046  trljat1  40131  trljat2  40132  ltrnatlw  40148  trlval4  40153  cdlemc1  40156  cdlemc3  40158  cdlemc6  40161  cdlemd3  40165  cdlemd4  40166  cdlemd5  40167  cdlemd6  40168  cdlemd7  40169  cdleme00a  40174  cdleme0cp  40179  cdleme0cq  40180  cdleme0e  40182  cdleme02N  40187  cdleme0ex2N  40189  cdleme0moN  40190  cdleme1  40192  cdleme2  40193  cdleme3e  40197  cdleme3g  40199  cdleme3h  40200  cdleme4  40203  cdleme5  40205  cdleme7aa  40207  cdleme7c  40210  cdleme7d  40211  cdleme7e  40212  cdleme8  40215  cdleme9  40218  cdleme10  40219  cdleme16aN  40224  cdleme11a  40225  cdleme11c  40226  cdleme11dN  40227  cdleme11e  40228  cdleme11g  40230  cdleme11h  40231  cdleme11j  40232  cdleme11k  40233  cdleme12  40236  cdleme15a  40239  cdleme15b  40240  cdleme16b  40244  cdleme17c  40253  cdleme0nex  40255  cdleme18d  40260  cdlemednpq  40264  cdleme20zN  40266  cdleme20y  40267  cdleme19a  40268  cdleme19d  40271  cdleme20aN  40274  cdleme20c  40276  cdleme20i  40282  cdleme20j  40283  cdleme21a  40290  cdleme21b  40291  cdleme21c  40292  cdleme21ct  40294  cdleme22cN  40307  cdleme22d  40308  cdleme22e  40309  cdleme22eALTN  40310  cdleme22f  40311  cdleme22f2  40312  cdleme22g  40313  cdleme23c  40316  cdleme41sn3a  40398  cdleme32le  40412  cdleme35b  40415  cdleme35c  40416  cdleme35d  40417  cdleme35e  40418  cdleme36a  40425  cdleme37m  40427  cdleme39a  40430  cdleme42a  40436  cdleme17d2  40460  cdlemeg46frv  40490  cdlemeg46rgv  40493  cdlemf1  40526  cdlemg2fv2  40565  cdlemg2l  40568  cdlemg2m  40569  cdlemg4d  40578  cdlemg4e  40579  cdlemg4f  40580  cdlemg4  40582  cdlemg6c  40585  cdlemg9a  40597  cdlemg10bALTN  40601  cdlemg12a  40608  cdlemg13  40617  cdlemg14f  40618  cdlemg14g  40619  cdlemg17i  40634  cdlemg17pq  40637  cdlemg19  40649  cdlemg21  40651  cdlemg27b  40661  cdlemg33c  40673  cdlemg33d  40674  trlcoabs2N  40687  cdlemg43  40695  cdlemg44b  40697  cdlemg44  40698  cdlemh1  40780  cdlemh2  40781  cdlemi1  40783  tendo0mul  40791  tendo0mulr  40792  cdlemk4  40799  cdlemk9  40804  cdlemk9bN  40805  cdlemk14  40819  cdlemkfid1N  40886  cdlemkid1  40887  cdlemk35s-id  40903  cdlemk39s-id  40905  cdlemk55a  40924  cdlemk55u  40931  cdlemk39u  40933  cdlemk19u  40935  cdlemk56  40936  cdleml8  40948  dia2dimlem1  41029  dia2dimlem2  41030  dia2dimlem3  41031  cdlemn10  41171  dihjust  41182  dihord1  41183  dihlsscpre  41199  dihvalcqpre  41200  dihglbcpreN  41265  dihmeetlem5  41273  dihmeetlem7N  41275  dihjatc1  41276  gpg3nbgrvtxlem  48017  lincreslvec3  48406  isldepslvec2  48409