Theorem syl131anc 1495

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

Syntax hints:   → wi 4   ∧ w3a 1100

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 198  df-an 385  df-3an 1102

This theorem is referenced by:  syl132anc  1500  syl231anc  1502  syl133anc  1505  initoeu2lem1  16866  estrresOLD  16981  estrres  16982  mulgdir  17774  2pthfrgr  27457  omndadd2d  30031  omndadd2rd  30032  submomnd  30033  omndmul2  30035  omndmul3  30036  ogrpinvOLD  30038  ogrpinv0le  30039  ogrpsub  30040  ogrpaddltbi  30042  ogrpaddltrd  30043  ogrpinv0lt  30046  isarchi3  30064  archirngz  30066  archiabllem1a  30068  archiabllem1b  30069  archiabllem2a  30071  archiabllem2c  30072  orngsqr  30127  ornglmulle  30128  orngrmulle  30129  ofldchr  30137  lineext  32502  brsegle2  32535  cvrcmp  35061  cvrcmp2  35062  atcvreq0  35092  cvlatexch3  35116  cvlcvr1  35117  cvlsupr2  35121  cvlsupr7  35126  atnlej1  35157  atnlej2  35158  cvrval3  35191  ltltncvr  35201  atcvrneN  35208  atcvrj2b  35210  atbtwnex  35226  3noncolr2  35227  3noncolr1N  35228  4noncolr3  35231  3dimlem2  35237  3dimlem3a  35238  3dimlem3  35239  3dimlem3OLDN  35240  3dimlem4a  35241  3dimlem4  35242  3dimlem4OLDN  35243  ps-1  35255  hlatexch4  35259  3atlem1  35261  3atlem2  35262  3atlem3  35263  3atlem4  35264  3atlem5  35265  3atlem6  35266  3atlem7  35267  2llnmat  35302  ps-2c  35306  lplnri3N  35333  lplnexllnN  35342  2llnmeqat  35349  4atlem0a  35371  4atlem0ae  35372  4atlem0be  35373  4atlem9  35381  4atlem10a  35382  4atlem10b  35383  4atlem10  35384  4atlem11a  35385  4atlem11  35387  4atlem12a  35388  dalemcnes  35428  dalempnes  35429  dalemqnet  35430  dalem1  35437  dalemdea  35440  dalem3  35442  dalem5  35445  dalem-cly  35449  dalem27  35477  dalem28  35478  dalem41  35491  dalem45  35495  dalem48  35498  lneq2at  35556  2lnat  35562  2llnma1  35565  2llnma3r  35566  2llnma2  35567  cdlemblem  35571  paddasslem2  35599  pmodl42N  35629  hlmod1i  35634  atmod1i1m  35636  atmod2i1  35639  atmod2i2  35640  atmod3i1  35642  llnexchb2lem  35646  dalawlem2  35650  dalawlem3  35651  dalawlem6  35654  dalawlem7  35655  dalawlem11  35659  dalawlem12  35660  pexmidlem3N  35750  lhpexle3lem  35789  lhpmcvr3  35803  lhp2at0  35810  lhpelim  35815  lhpmod2i2  35816  lhpmod6i1  35817  4atexlempns  35840  4atexlemunv  35844  4atexlemc  35847  4atexlemnclw  35848  4atexlemex2  35849  4atexlemex6  35852  4atex  35854  4atex3  35859  trljat1  35945  trljat2  35946  ltrnatlw  35962  trlval4  35967  cdlemc1  35970  cdlemc3  35972  cdlemc6  35975  cdlemd3  35979  cdlemd4  35980  cdlemd5  35981  cdlemd6  35982  cdlemd7  35983  cdleme00a  35988  cdleme0cp  35993  cdleme0cq  35994  cdleme0e  35996  cdleme02N  36001  cdleme0ex2N  36003  cdleme0moN  36004  cdleme1  36006  cdleme2  36007  cdleme3e  36011  cdleme3g  36013  cdleme3h  36014  cdleme4  36017  cdleme5  36019  cdleme7aa  36021  cdleme7c  36024  cdleme7d  36025  cdleme7e  36026  cdleme8  36029  cdleme9  36032  cdleme10  36033  cdleme16aN  36038  cdleme11a  36039  cdleme11c  36040  cdleme11dN  36041  cdleme11e  36042  cdleme11g  36044  cdleme11h  36045  cdleme11j  36046  cdleme11k  36047  cdleme12  36050  cdleme15a  36053  cdleme15b  36054  cdleme16b  36058  cdleme17c  36067  cdleme0nex  36069  cdleme18d  36074  cdlemednpq  36078  cdleme20zN  36080  cdleme20y  36081  cdleme19a  36082  cdleme19d  36085  cdleme20aN  36088  cdleme20c  36090  cdleme20i  36096  cdleme20j  36097  cdleme21a  36104  cdleme21b  36105  cdleme21c  36106  cdleme21ct  36108  cdleme22cN  36121  cdleme22d  36122  cdleme22e  36123  cdleme22eALTN  36124  cdleme22f  36125  cdleme22f2  36126  cdleme22g  36127  cdleme23c  36130  cdleme41sn3a  36212  cdleme32le  36226  cdleme35b  36229  cdleme35c  36230  cdleme35d  36231  cdleme35e  36232  cdleme36a  36239  cdleme37m  36241  cdleme39a  36244  cdleme42a  36250  cdleme17d2  36274  cdlemeg46frv  36304  cdlemeg46rgv  36307  cdlemf1  36340  cdlemg2fv2  36379  cdlemg2l  36382  cdlemg2m  36383  cdlemg4d  36392  cdlemg4e  36393  cdlemg4f  36394  cdlemg4  36396  cdlemg6c  36399  cdlemg9a  36411  cdlemg10bALTN  36415  cdlemg12a  36422  cdlemg13  36431  cdlemg14f  36432  cdlemg14g  36433  cdlemg17i  36448  cdlemg17pq  36451  cdlemg19  36463  cdlemg21  36465  cdlemg27b  36475  cdlemg33c  36487  cdlemg33d  36488  trlcoabs2N  36501  cdlemg43  36509  cdlemg44b  36511  cdlemg44  36512  cdlemh1  36594  cdlemh2  36595  cdlemi1  36597  tendo0mul  36605  tendo0mulr  36606  cdlemk4  36613  cdlemk9  36618  cdlemk9bN  36619  cdlemk14  36633  cdlemkfid1N  36700  cdlemkid1  36701  cdlemk35s-id  36717  cdlemk39s-id  36719  cdlemk55a  36738  cdlemk55u  36745  cdlemk39u  36747  cdlemk19u  36749  cdlemk56  36750  cdleml8  36762  dia2dimlem1  36843  dia2dimlem2  36844  dia2dimlem3  36845  cdlemn10  36985  dihjust  36996  dihord1  36997  dihlsscpre  37013  dihvalcqpre  37014  dihglbcpreN  37079  dihmeetlem5  37087  dihmeetlem7N  37089  dihjatc1  37090  lincreslvec3  42837  isldepslvec2  42840