Theorem syl131anc 1401

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

Syntax hints:   → wi 4   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  syl132anc  1406  syl231anc  1408  syl133anc  1411  initoeu2lem1  18030  estrres  18154  mulgdir  19131  omndadd2d  20153  omndadd2rd  20154  submomnd  20155  omndmul2  20156  omndmul3  20157  ogrpinv0le  20159  ogrpsub  20160  ogrpaddltbi  20162  ogrpaddltrd  20163  ogrpinv0lt  20166  orngsqr  20895  ornglmulle  20896  orngrmulle  20897  ofldchr  21608  umgr2edg  29356  2pthfrgr  30432  isarchi3  33328  archirngz  33330  archiabllem1a  33332  archiabllem1b  33333  archiabllem2a  33335  archiabllem2c  33336  lineext  36390  brsegle2  36423  cvrcmp  39871  cvrcmp2  39872  atcvreq0  39902  cvlatexch3  39926  cvlcvr1  39927  cvlsupr2  39931  cvlsupr7  39936  atnlej1  39967  atnlej2  39968  cvrval3  40001  ltltncvr  40011  atcvrneN  40018  atcvrj2b  40020  atbtwnex  40036  3noncolr2  40037  3noncolr1N  40038  4noncolr3  40041  3dimlem2  40047  3dimlem3a  40048  3dimlem3  40049  3dimlem3OLDN  40050  3dimlem4a  40051  3dimlem4  40052  3dimlem4OLDN  40053  ps-1  40065  hlatexch4  40069  3atlem1  40071  3atlem2  40072  3atlem3  40073  3atlem4  40074  3atlem5  40075  3atlem6  40076  3atlem7  40077  2llnmat  40112  ps-2c  40116  lplnri3N  40143  lplnexllnN  40152  2llnmeqat  40159  4atlem0a  40181  4atlem0ae  40182  4atlem0be  40183  4atlem9  40191  4atlem10a  40192  4atlem10b  40193  4atlem10  40194  4atlem11a  40195  4atlem11  40197  4atlem12a  40198  dalemcnes  40238  dalempnes  40239  dalemqnet  40240  dalem1  40247  dalemdea  40250  dalem3  40252  dalem5  40255  dalem-cly  40259  dalem27  40287  dalem28  40288  dalem41  40301  dalem45  40305  dalem48  40308  lneq2at  40366  2lnat  40372  2llnma1  40375  2llnma3r  40376  2llnma2  40377  cdlemblem  40381  paddasslem2  40409  pmodl42N  40439  hlmod1i  40444  atmod1i1m  40446  atmod2i1  40449  atmod2i2  40450  atmod3i1  40452  llnexchb2lem  40456  dalawlem2  40460  dalawlem3  40461  dalawlem6  40464  dalawlem7  40465  dalawlem11  40469  dalawlem12  40470  pexmidlem3N  40560  lhpexle3lem  40599  lhpmcvr3  40613  lhp2at0  40620  lhpelim  40625  lhpmod2i2  40626  lhpmod6i1  40627  4atexlempns  40650  4atexlemunv  40654  4atexlemc  40657  4atexlemnclw  40658  4atexlemex2  40659  4atexlemex6  40662  4atex  40664  4atex3  40669  trljat1  40754  trljat2  40755  ltrnatlw  40771  trlval4  40776  cdlemc1  40779  cdlemc3  40781  cdlemc6  40784  cdlemd3  40788  cdlemd4  40789  cdlemd5  40790  cdlemd6  40791  cdlemd7  40792  cdleme00a  40797  cdleme0cp  40802  cdleme0cq  40803  cdleme0e  40805  cdleme02N  40810  cdleme0ex2N  40812  cdleme0moN  40813  cdleme1  40815  cdleme2  40816  cdleme3e  40820  cdleme3g  40822  cdleme3h  40823  cdleme4  40826  cdleme5  40828  cdleme7aa  40830  cdleme7c  40833  cdleme7d  40834  cdleme7e  40835  cdleme8  40838  cdleme9  40841  cdleme10  40842  cdleme16aN  40847  cdleme11a  40848  cdleme11c  40849  cdleme11dN  40850  cdleme11e  40851  cdleme11g  40853  cdleme11h  40854  cdleme11j  40855  cdleme11k  40856  cdleme12  40859  cdleme15a  40862  cdleme15b  40863  cdleme16b  40867  cdleme17c  40876  cdleme0nex  40878  cdleme18d  40883  cdlemednpq  40887  cdleme20zN  40889  cdleme20y  40890  cdleme19a  40891  cdleme19d  40894  cdleme20aN  40897  cdleme20c  40899  cdleme20i  40905  cdleme20j  40906  cdleme21a  40913  cdleme21b  40914  cdleme21c  40915  cdleme21ct  40917  cdleme22cN  40930  cdleme22d  40931  cdleme22e  40932  cdleme22eALTN  40933  cdleme22f  40934  cdleme22f2  40935  cdleme22g  40936  cdleme23c  40939  cdleme41sn3a  41021  cdleme32le  41035  cdleme35b  41038  cdleme35c  41039  cdleme35d  41040  cdleme35e  41041  cdleme36a  41048  cdleme37m  41050  cdleme39a  41053  cdleme42a  41059  cdleme17d2  41083  cdlemeg46frv  41113  cdlemeg46rgv  41116  cdlemf1  41149  cdlemg2fv2  41188  cdlemg2l  41191  cdlemg2m  41192  cdlemg4d  41201  cdlemg4e  41202  cdlemg4f  41203  cdlemg4  41205  cdlemg6c  41208  cdlemg9a  41220  cdlemg10bALTN  41224  cdlemg12a  41231  cdlemg13  41240  cdlemg14f  41241  cdlemg14g  41242  cdlemg17i  41257  cdlemg17pq  41260  cdlemg19  41272  cdlemg21  41274  cdlemg27b  41284  cdlemg33c  41296  cdlemg33d  41297  trlcoabs2N  41310  cdlemg43  41318  cdlemg44b  41320  cdlemg44  41321  cdlemh1  41403  cdlemh2  41404  cdlemi1  41406  tendo0mul  41414  tendo0mulr  41415  cdlemk4  41422  cdlemk9  41427  cdlemk9bN  41428  cdlemk14  41442  cdlemkfid1N  41509  cdlemkid1  41510  cdlemk35s-id  41526  cdlemk39s-id  41528  cdlemk55a  41547  cdlemk55u  41554  cdlemk39u  41556  cdlemk19u  41558  cdlemk56  41559  cdleml8  41571  dia2dimlem1  41652  dia2dimlem2  41653  dia2dimlem3  41654  cdlemn10  41794  dihjust  41805  dihord1  41806  dihlsscpre  41822  dihvalcqpre  41823  dihglbcpreN  41888  dihmeetlem5  41896  dihmeetlem7N  41898  dihjatc1  41899  modmknepk  47926  modm2nep1  47930  modp2nep1  47931  modm1nep2  47932  modm1nem2  47933  lincreslvec3  49068  isldepslvec2  49071