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  17950  estrres  18074  mulgdir  19048  omndadd2d  20071  omndadd2rd  20072  submomnd  20073  omndmul2  20074  omndmul3  20075  ogrpinv0le  20077  ogrpsub  20078  ogrpaddltbi  20080  ogrpaddltrd  20081  ogrpinv0lt  20084  orngsqr  20811  ornglmulle  20812  orngrmulle  20813  ofldchr  21543  umgr2edg  29294  2pthfrgr  30371  isarchi3  33280  archirngz  33282  archiabllem1a  33284  archiabllem1b  33285  archiabllem2a  33287  archiabllem2c  33288  lineext  36289  brsegle2  36322  cvrcmp  39653  cvrcmp2  39654  atcvreq0  39684  cvlatexch3  39708  cvlcvr1  39709  cvlsupr2  39713  cvlsupr7  39718  atnlej1  39749  atnlej2  39750  cvrval3  39783  ltltncvr  39793  atcvrneN  39800  atcvrj2b  39802  atbtwnex  39818  3noncolr2  39819  3noncolr1N  39820  4noncolr3  39823  3dimlem2  39829  3dimlem3a  39830  3dimlem3  39831  3dimlem3OLDN  39832  3dimlem4a  39833  3dimlem4  39834  3dimlem4OLDN  39835  ps-1  39847  hlatexch4  39851  3atlem1  39853  3atlem2  39854  3atlem3  39855  3atlem4  39856  3atlem5  39857  3atlem6  39858  3atlem7  39859  2llnmat  39894  ps-2c  39898  lplnri3N  39925  lplnexllnN  39934  2llnmeqat  39941  4atlem0a  39963  4atlem0ae  39964  4atlem0be  39965  4atlem9  39973  4atlem10a  39974  4atlem10b  39975  4atlem10  39976  4atlem11a  39977  4atlem11  39979  4atlem12a  39980  dalemcnes  40020  dalempnes  40021  dalemqnet  40022  dalem1  40029  dalemdea  40032  dalem3  40034  dalem5  40037  dalem-cly  40041  dalem27  40069  dalem28  40070  dalem41  40083  dalem45  40087  dalem48  40090  lneq2at  40148  2lnat  40154  2llnma1  40157  2llnma3r  40158  2llnma2  40159  cdlemblem  40163  paddasslem2  40191  pmodl42N  40221  hlmod1i  40226  atmod1i1m  40228  atmod2i1  40231  atmod2i2  40232  atmod3i1  40234  llnexchb2lem  40238  dalawlem2  40242  dalawlem3  40243  dalawlem6  40246  dalawlem7  40247  dalawlem11  40251  dalawlem12  40252  pexmidlem3N  40342  lhpexle3lem  40381  lhpmcvr3  40395  lhp2at0  40402  lhpelim  40407  lhpmod2i2  40408  lhpmod6i1  40409  4atexlempns  40432  4atexlemunv  40436  4atexlemc  40439  4atexlemnclw  40440  4atexlemex2  40441  4atexlemex6  40444  4atex  40446  4atex3  40451  trljat1  40536  trljat2  40537  ltrnatlw  40553  trlval4  40558  cdlemc1  40561  cdlemc3  40563  cdlemc6  40566  cdlemd3  40570  cdlemd4  40571  cdlemd5  40572  cdlemd6  40573  cdlemd7  40574  cdleme00a  40579  cdleme0cp  40584  cdleme0cq  40585  cdleme0e  40587  cdleme02N  40592  cdleme0ex2N  40594  cdleme0moN  40595  cdleme1  40597  cdleme2  40598  cdleme3e  40602  cdleme3g  40604  cdleme3h  40605  cdleme4  40608  cdleme5  40610  cdleme7aa  40612  cdleme7c  40615  cdleme7d  40616  cdleme7e  40617  cdleme8  40620  cdleme9  40623  cdleme10  40624  cdleme16aN  40629  cdleme11a  40630  cdleme11c  40631  cdleme11dN  40632  cdleme11e  40633  cdleme11g  40635  cdleme11h  40636  cdleme11j  40637  cdleme11k  40638  cdleme12  40641  cdleme15a  40644  cdleme15b  40645  cdleme16b  40649  cdleme17c  40658  cdleme0nex  40660  cdleme18d  40665  cdlemednpq  40669  cdleme20zN  40671  cdleme20y  40672  cdleme19a  40673  cdleme19d  40676  cdleme20aN  40679  cdleme20c  40681  cdleme20i  40687  cdleme20j  40688  cdleme21a  40695  cdleme21b  40696  cdleme21c  40697  cdleme21ct  40699  cdleme22cN  40712  cdleme22d  40713  cdleme22e  40714  cdleme22eALTN  40715  cdleme22f  40716  cdleme22f2  40717  cdleme22g  40718  cdleme23c  40721  cdleme41sn3a  40803  cdleme32le  40817  cdleme35b  40820  cdleme35c  40821  cdleme35d  40822  cdleme35e  40823  cdleme36a  40830  cdleme37m  40832  cdleme39a  40835  cdleme42a  40841  cdleme17d2  40865  cdlemeg46frv  40895  cdlemeg46rgv  40898  cdlemf1  40931  cdlemg2fv2  40970  cdlemg2l  40973  cdlemg2m  40974  cdlemg4d  40983  cdlemg4e  40984  cdlemg4f  40985  cdlemg4  40987  cdlemg6c  40990  cdlemg9a  41002  cdlemg10bALTN  41006  cdlemg12a  41013  cdlemg13  41022  cdlemg14f  41023  cdlemg14g  41024  cdlemg17i  41039  cdlemg17pq  41042  cdlemg19  41054  cdlemg21  41056  cdlemg27b  41066  cdlemg33c  41078  cdlemg33d  41079  trlcoabs2N  41092  cdlemg43  41100  cdlemg44b  41102  cdlemg44  41103  cdlemh1  41185  cdlemh2  41186  cdlemi1  41188  tendo0mul  41196  tendo0mulr  41197  cdlemk4  41204  cdlemk9  41209  cdlemk9bN  41210  cdlemk14  41224  cdlemkfid1N  41291  cdlemkid1  41292  cdlemk35s-id  41308  cdlemk39s-id  41310  cdlemk55a  41329  cdlemk55u  41336  cdlemk39u  41338  cdlemk19u  41340  cdlemk56  41341  cdleml8  41353  dia2dimlem1  41434  dia2dimlem2  41435  dia2dimlem3  41436  cdlemn10  41576  dihjust  41587  dihord1  41588  dihlsscpre  41604  dihvalcqpre  41605  dihglbcpreN  41670  dihmeetlem5  41678  dihmeetlem7N  41680  dihjatc1  41681  modmknepk  47716  modm2nep1  47720  modp2nep1  47721  modm1nep2  47722  modm1nem2  47723  lincreslvec3  48836  isldepslvec2  48839