Theorem syl131anc 1384

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 1372	1 ⊢ (𝜑 → 𝜁)

Syntax hints:   → wi 4   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  syl132anc  1389  syl231anc  1391  syl133anc  1394  initoeu2lem1  17964  estrres  18091  mulgdir  18986  umgr2edg  28466  2pthfrgr  29537  omndadd2d  32226  omndadd2rd  32227  submomnd  32228  omndmul2  32230  omndmul3  32231  ogrpinv0le  32233  ogrpsub  32234  ogrpaddltbi  32236  ogrpaddltrd  32237  ogrpinv0lt  32240  isarchi3  32333  archirngz  32335  archiabllem1a  32337  archiabllem1b  32338  archiabllem2a  32340  archiabllem2c  32341  orngsqr  32422  ornglmulle  32423  orngrmulle  32424  ofldchr  32432  lineext  35048  brsegle2  35081  cvrcmp  38153  cvrcmp2  38154  atcvreq0  38184  cvlatexch3  38208  cvlcvr1  38209  cvlsupr2  38213  cvlsupr7  38218  atnlej1  38250  atnlej2  38251  cvrval3  38284  ltltncvr  38294  atcvrneN  38301  atcvrj2b  38303  atbtwnex  38319  3noncolr2  38320  3noncolr1N  38321  4noncolr3  38324  3dimlem2  38330  3dimlem3a  38331  3dimlem3  38332  3dimlem3OLDN  38333  3dimlem4a  38334  3dimlem4  38335  3dimlem4OLDN  38336  ps-1  38348  hlatexch4  38352  3atlem1  38354  3atlem2  38355  3atlem3  38356  3atlem4  38357  3atlem5  38358  3atlem6  38359  3atlem7  38360  2llnmat  38395  ps-2c  38399  lplnri3N  38426  lplnexllnN  38435  2llnmeqat  38442  4atlem0a  38464  4atlem0ae  38465  4atlem0be  38466  4atlem9  38474  4atlem10a  38475  4atlem10b  38476  4atlem10  38477  4atlem11a  38478  4atlem11  38480  4atlem12a  38481  dalemcnes  38521  dalempnes  38522  dalemqnet  38523  dalem1  38530  dalemdea  38533  dalem3  38535  dalem5  38538  dalem-cly  38542  dalem27  38570  dalem28  38571  dalem41  38584  dalem45  38588  dalem48  38591  lneq2at  38649  2lnat  38655  2llnma1  38658  2llnma3r  38659  2llnma2  38660  cdlemblem  38664  paddasslem2  38692  pmodl42N  38722  hlmod1i  38727  atmod1i1m  38729  atmod2i1  38732  atmod2i2  38733  atmod3i1  38735  llnexchb2lem  38739  dalawlem2  38743  dalawlem3  38744  dalawlem6  38747  dalawlem7  38748  dalawlem11  38752  dalawlem12  38753  pexmidlem3N  38843  lhpexle3lem  38882  lhpmcvr3  38896  lhp2at0  38903  lhpelim  38908  lhpmod2i2  38909  lhpmod6i1  38910  4atexlempns  38933  4atexlemunv  38937  4atexlemc  38940  4atexlemnclw  38941  4atexlemex2  38942  4atexlemex6  38945  4atex  38947  4atex3  38952  trljat1  39037  trljat2  39038  ltrnatlw  39054  trlval4  39059  cdlemc1  39062  cdlemc3  39064  cdlemc6  39067  cdlemd3  39071  cdlemd4  39072  cdlemd5  39073  cdlemd6  39074  cdlemd7  39075  cdleme00a  39080  cdleme0cp  39085  cdleme0cq  39086  cdleme0e  39088  cdleme02N  39093  cdleme0ex2N  39095  cdleme0moN  39096  cdleme1  39098  cdleme2  39099  cdleme3e  39103  cdleme3g  39105  cdleme3h  39106  cdleme4  39109  cdleme5  39111  cdleme7aa  39113  cdleme7c  39116  cdleme7d  39117  cdleme7e  39118  cdleme8  39121  cdleme9  39124  cdleme10  39125  cdleme16aN  39130  cdleme11a  39131  cdleme11c  39132  cdleme11dN  39133  cdleme11e  39134  cdleme11g  39136  cdleme11h  39137  cdleme11j  39138  cdleme11k  39139  cdleme12  39142  cdleme15a  39145  cdleme15b  39146  cdleme16b  39150  cdleme17c  39159  cdleme0nex  39161  cdleme18d  39166  cdlemednpq  39170  cdleme20zN  39172  cdleme20y  39173  cdleme19a  39174  cdleme19d  39177  cdleme20aN  39180  cdleme20c  39182  cdleme20i  39188  cdleme20j  39189  cdleme21a  39196  cdleme21b  39197  cdleme21c  39198  cdleme21ct  39200  cdleme22cN  39213  cdleme22d  39214  cdleme22e  39215  cdleme22eALTN  39216  cdleme22f  39217  cdleme22f2  39218  cdleme22g  39219  cdleme23c  39222  cdleme41sn3a  39304  cdleme32le  39318  cdleme35b  39321  cdleme35c  39322  cdleme35d  39323  cdleme35e  39324  cdleme36a  39331  cdleme37m  39333  cdleme39a  39336  cdleme42a  39342  cdleme17d2  39366  cdlemeg46frv  39396  cdlemeg46rgv  39399  cdlemf1  39432  cdlemg2fv2  39471  cdlemg2l  39474  cdlemg2m  39475  cdlemg4d  39484  cdlemg4e  39485  cdlemg4f  39486  cdlemg4  39488  cdlemg6c  39491  cdlemg9a  39503  cdlemg10bALTN  39507  cdlemg12a  39514  cdlemg13  39523  cdlemg14f  39524  cdlemg14g  39525  cdlemg17i  39540  cdlemg17pq  39543  cdlemg19  39555  cdlemg21  39557  cdlemg27b  39567  cdlemg33c  39579  cdlemg33d  39580  trlcoabs2N  39593  cdlemg43  39601  cdlemg44b  39603  cdlemg44  39604  cdlemh1  39686  cdlemh2  39687  cdlemi1  39689  tendo0mul  39697  tendo0mulr  39698  cdlemk4  39705  cdlemk9  39710  cdlemk9bN  39711  cdlemk14  39725  cdlemkfid1N  39792  cdlemkid1  39793  cdlemk35s-id  39809  cdlemk39s-id  39811  cdlemk55a  39830  cdlemk55u  39837  cdlemk39u  39839  cdlemk19u  39841  cdlemk56  39842  cdleml8  39854  dia2dimlem1  39935  dia2dimlem2  39936  dia2dimlem3  39937  cdlemn10  40077  dihjust  40088  dihord1  40089  dihlsscpre  40105  dihvalcqpre  40106  dihglbcpreN  40171  dihmeetlem5  40179  dihmeetlem7N  40181  dihjatc1  40182  lincreslvec3  47163  isldepslvec2  47166