Theorem syl131anc 1386

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 1129	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃 ∧ 𝜏))
6		syl23anc.5	. 2 ⊢ (𝜑 → 𝜂)
7		syl131anc.6	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁)
8	1, 5, 6, 7	syl3anc 1374	1 ⊢ (𝜑 → 𝜁)

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  syl132anc  1391  syl231anc  1393  syl133anc  1396  initoeu2lem1  17981  estrres  18105  mulgdir  19082  omndadd2d  20105  omndadd2rd  20106  submomnd  20107  omndmul2  20108  omndmul3  20109  ogrpinv0le  20111  ogrpsub  20112  ogrpaddltbi  20114  ogrpaddltrd  20115  ogrpinv0lt  20118  orngsqr  20843  ornglmulle  20844  orngrmulle  20845  ofldchr  21556  umgr2edg  29278  2pthfrgr  30354  isarchi3  33248  archirngz  33250  archiabllem1a  33252  archiabllem1b  33253  archiabllem2a  33255  archiabllem2c  33256  lineext  36258  brsegle2  36291  cvrcmp  39729  cvrcmp2  39730  atcvreq0  39760  cvlatexch3  39784  cvlcvr1  39785  cvlsupr2  39789  cvlsupr7  39794  atnlej1  39825  atnlej2  39826  cvrval3  39859  ltltncvr  39869  atcvrneN  39876  atcvrj2b  39878  atbtwnex  39894  3noncolr2  39895  3noncolr1N  39896  4noncolr3  39899  3dimlem2  39905  3dimlem3a  39906  3dimlem3  39907  3dimlem3OLDN  39908  3dimlem4a  39909  3dimlem4  39910  3dimlem4OLDN  39911  ps-1  39923  hlatexch4  39927  3atlem1  39929  3atlem2  39930  3atlem3  39931  3atlem4  39932  3atlem5  39933  3atlem6  39934  3atlem7  39935  2llnmat  39970  ps-2c  39974  lplnri3N  40001  lplnexllnN  40010  2llnmeqat  40017  4atlem0a  40039  4atlem0ae  40040  4atlem0be  40041  4atlem9  40049  4atlem10a  40050  4atlem10b  40051  4atlem10  40052  4atlem11a  40053  4atlem11  40055  4atlem12a  40056  dalemcnes  40096  dalempnes  40097  dalemqnet  40098  dalem1  40105  dalemdea  40108  dalem3  40110  dalem5  40113  dalem-cly  40117  dalem27  40145  dalem28  40146  dalem41  40159  dalem45  40163  dalem48  40166  lneq2at  40224  2lnat  40230  2llnma1  40233  2llnma3r  40234  2llnma2  40235  cdlemblem  40239  paddasslem2  40267  pmodl42N  40297  hlmod1i  40302  atmod1i1m  40304  atmod2i1  40307  atmod2i2  40308  atmod3i1  40310  llnexchb2lem  40314  dalawlem2  40318  dalawlem3  40319  dalawlem6  40322  dalawlem7  40323  dalawlem11  40327  dalawlem12  40328  pexmidlem3N  40418  lhpexle3lem  40457  lhpmcvr3  40471  lhp2at0  40478  lhpelim  40483  lhpmod2i2  40484  lhpmod6i1  40485  4atexlempns  40508  4atexlemunv  40512  4atexlemc  40515  4atexlemnclw  40516  4atexlemex2  40517  4atexlemex6  40520  4atex  40522  4atex3  40527  trljat1  40612  trljat2  40613  ltrnatlw  40629  trlval4  40634  cdlemc1  40637  cdlemc3  40639  cdlemc6  40642  cdlemd3  40646  cdlemd4  40647  cdlemd5  40648  cdlemd6  40649  cdlemd7  40650  cdleme00a  40655  cdleme0cp  40660  cdleme0cq  40661  cdleme0e  40663  cdleme02N  40668  cdleme0ex2N  40670  cdleme0moN  40671  cdleme1  40673  cdleme2  40674  cdleme3e  40678  cdleme3g  40680  cdleme3h  40681  cdleme4  40684  cdleme5  40686  cdleme7aa  40688  cdleme7c  40691  cdleme7d  40692  cdleme7e  40693  cdleme8  40696  cdleme9  40699  cdleme10  40700  cdleme16aN  40705  cdleme11a  40706  cdleme11c  40707  cdleme11dN  40708  cdleme11e  40709  cdleme11g  40711  cdleme11h  40712  cdleme11j  40713  cdleme11k  40714  cdleme12  40717  cdleme15a  40720  cdleme15b  40721  cdleme16b  40725  cdleme17c  40734  cdleme0nex  40736  cdleme18d  40741  cdlemednpq  40745  cdleme20zN  40747  cdleme20y  40748  cdleme19a  40749  cdleme19d  40752  cdleme20aN  40755  cdleme20c  40757  cdleme20i  40763  cdleme20j  40764  cdleme21a  40771  cdleme21b  40772  cdleme21c  40773  cdleme21ct  40775  cdleme22cN  40788  cdleme22d  40789  cdleme22e  40790  cdleme22eALTN  40791  cdleme22f  40792  cdleme22f2  40793  cdleme22g  40794  cdleme23c  40797  cdleme41sn3a  40879  cdleme32le  40893  cdleme35b  40896  cdleme35c  40897  cdleme35d  40898  cdleme35e  40899  cdleme36a  40906  cdleme37m  40908  cdleme39a  40911  cdleme42a  40917  cdleme17d2  40941  cdlemeg46frv  40971  cdlemeg46rgv  40974  cdlemf1  41007  cdlemg2fv2  41046  cdlemg2l  41049  cdlemg2m  41050  cdlemg4d  41059  cdlemg4e  41060  cdlemg4f  41061  cdlemg4  41063  cdlemg6c  41066  cdlemg9a  41078  cdlemg10bALTN  41082  cdlemg12a  41089  cdlemg13  41098  cdlemg14f  41099  cdlemg14g  41100  cdlemg17i  41115  cdlemg17pq  41118  cdlemg19  41130  cdlemg21  41132  cdlemg27b  41142  cdlemg33c  41154  cdlemg33d  41155  trlcoabs2N  41168  cdlemg43  41176  cdlemg44b  41178  cdlemg44  41179  cdlemh1  41261  cdlemh2  41262  cdlemi1  41264  tendo0mul  41272  tendo0mulr  41273  cdlemk4  41280  cdlemk9  41285  cdlemk9bN  41286  cdlemk14  41300  cdlemkfid1N  41367  cdlemkid1  41368  cdlemk35s-id  41384  cdlemk39s-id  41386  cdlemk55a  41405  cdlemk55u  41412  cdlemk39u  41414  cdlemk19u  41416  cdlemk56  41417  cdleml8  41429  dia2dimlem1  41510  dia2dimlem2  41511  dia2dimlem3  41512  cdlemn10  41652  dihjust  41663  dihord1  41664  dihlsscpre  41680  dihvalcqpre  41681  dihglbcpreN  41746  dihmeetlem5  41754  dihmeetlem7N  41756  dihjatc1  41757  modmknepk  47816  modm2nep1  47820  modp2nep1  47821  modm1nep2  47822  modm1nem2  47823  lincreslvec3  48958  isldepslvec2  48961