Theorem syl131anc 1380

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

Syntax hints:   → wi 4   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  syl132anc  1385  syl231anc  1387  syl133anc  1390  initoeu2lem1  17266  estrres  17381  mulgdir  18251  umgr2edg  26999  2pthfrgr  28069  omndadd2d  30759  omndadd2rd  30760  submomnd  30761  omndmul2  30763  omndmul3  30764  ogrpinv0le  30766  ogrpsub  30767  ogrpaddltbi  30769  ogrpaddltrd  30770  ogrpinv0lt  30773  isarchi3  30866  archirngz  30868  archiabllem1a  30870  archiabllem1b  30871  archiabllem2a  30873  archiabllem2c  30874  orngsqr  30928  ornglmulle  30929  orngrmulle  30930  ofldchr  30938  lineext  33650  brsegle2  33683  cvrcmp  36579  cvrcmp2  36580  atcvreq0  36610  cvlatexch3  36634  cvlcvr1  36635  cvlsupr2  36639  cvlsupr7  36644  atnlej1  36675  atnlej2  36676  cvrval3  36709  ltltncvr  36719  atcvrneN  36726  atcvrj2b  36728  atbtwnex  36744  3noncolr2  36745  3noncolr1N  36746  4noncolr3  36749  3dimlem2  36755  3dimlem3a  36756  3dimlem3  36757  3dimlem3OLDN  36758  3dimlem4a  36759  3dimlem4  36760  3dimlem4OLDN  36761  ps-1  36773  hlatexch4  36777  3atlem1  36779  3atlem2  36780  3atlem3  36781  3atlem4  36782  3atlem5  36783  3atlem6  36784  3atlem7  36785  2llnmat  36820  ps-2c  36824  lplnri3N  36851  lplnexllnN  36860  2llnmeqat  36867  4atlem0a  36889  4atlem0ae  36890  4atlem0be  36891  4atlem9  36899  4atlem10a  36900  4atlem10b  36901  4atlem10  36902  4atlem11a  36903  4atlem11  36905  4atlem12a  36906  dalemcnes  36946  dalempnes  36947  dalemqnet  36948  dalem1  36955  dalemdea  36958  dalem3  36960  dalem5  36963  dalem-cly  36967  dalem27  36995  dalem28  36996  dalem41  37009  dalem45  37013  dalem48  37016  lneq2at  37074  2lnat  37080  2llnma1  37083  2llnma3r  37084  2llnma2  37085  cdlemblem  37089  paddasslem2  37117  pmodl42N  37147  hlmod1i  37152  atmod1i1m  37154  atmod2i1  37157  atmod2i2  37158  atmod3i1  37160  llnexchb2lem  37164  dalawlem2  37168  dalawlem3  37169  dalawlem6  37172  dalawlem7  37173  dalawlem11  37177  dalawlem12  37178  pexmidlem3N  37268  lhpexle3lem  37307  lhpmcvr3  37321  lhp2at0  37328  lhpelim  37333  lhpmod2i2  37334  lhpmod6i1  37335  4atexlempns  37358  4atexlemunv  37362  4atexlemc  37365  4atexlemnclw  37366  4atexlemex2  37367  4atexlemex6  37370  4atex  37372  4atex3  37377  trljat1  37462  trljat2  37463  ltrnatlw  37479  trlval4  37484  cdlemc1  37487  cdlemc3  37489  cdlemc6  37492  cdlemd3  37496  cdlemd4  37497  cdlemd5  37498  cdlemd6  37499  cdlemd7  37500  cdleme00a  37505  cdleme0cp  37510  cdleme0cq  37511  cdleme0e  37513  cdleme02N  37518  cdleme0ex2N  37520  cdleme0moN  37521  cdleme1  37523  cdleme2  37524  cdleme3e  37528  cdleme3g  37530  cdleme3h  37531  cdleme4  37534  cdleme5  37536  cdleme7aa  37538  cdleme7c  37541  cdleme7d  37542  cdleme7e  37543  cdleme8  37546  cdleme9  37549  cdleme10  37550  cdleme16aN  37555  cdleme11a  37556  cdleme11c  37557  cdleme11dN  37558  cdleme11e  37559  cdleme11g  37561  cdleme11h  37562  cdleme11j  37563  cdleme11k  37564  cdleme12  37567  cdleme15a  37570  cdleme15b  37571  cdleme16b  37575  cdleme17c  37584  cdleme0nex  37586  cdleme18d  37591  cdlemednpq  37595  cdleme20zN  37597  cdleme20y  37598  cdleme19a  37599  cdleme19d  37602  cdleme20aN  37605  cdleme20c  37607  cdleme20i  37613  cdleme20j  37614  cdleme21a  37621  cdleme21b  37622  cdleme21c  37623  cdleme21ct  37625  cdleme22cN  37638  cdleme22d  37639  cdleme22e  37640  cdleme22eALTN  37641  cdleme22f  37642  cdleme22f2  37643  cdleme22g  37644  cdleme23c  37647  cdleme41sn3a  37729  cdleme32le  37743  cdleme35b  37746  cdleme35c  37747  cdleme35d  37748  cdleme35e  37749  cdleme36a  37756  cdleme37m  37758  cdleme39a  37761  cdleme42a  37767  cdleme17d2  37791  cdlemeg46frv  37821  cdlemeg46rgv  37824  cdlemf1  37857  cdlemg2fv2  37896  cdlemg2l  37899  cdlemg2m  37900  cdlemg4d  37909  cdlemg4e  37910  cdlemg4f  37911  cdlemg4  37913  cdlemg6c  37916  cdlemg9a  37928  cdlemg10bALTN  37932  cdlemg12a  37939  cdlemg13  37948  cdlemg14f  37949  cdlemg14g  37950  cdlemg17i  37965  cdlemg17pq  37968  cdlemg19  37980  cdlemg21  37982  cdlemg27b  37992  cdlemg33c  38004  cdlemg33d  38005  trlcoabs2N  38018  cdlemg43  38026  cdlemg44b  38028  cdlemg44  38029  cdlemh1  38111  cdlemh2  38112  cdlemi1  38114  tendo0mul  38122  tendo0mulr  38123  cdlemk4  38130  cdlemk9  38135  cdlemk9bN  38136  cdlemk14  38150  cdlemkfid1N  38217  cdlemkid1  38218  cdlemk35s-id  38234  cdlemk39s-id  38236  cdlemk55a  38255  cdlemk55u  38262  cdlemk39u  38264  cdlemk19u  38266  cdlemk56  38267  cdleml8  38279  dia2dimlem1  38360  dia2dimlem2  38361  dia2dimlem3  38362  cdlemn10  38502  dihjust  38513  dihord1  38514  dihlsscpre  38530  dihvalcqpre  38531  dihglbcpreN  38596  dihmeetlem5  38604  dihmeetlem7N  38606  dihjatc1  38607  lincreslvec3  44891  isldepslvec2  44894