Theorem syl131anc 1383

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 1128	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃 ∧ 𝜏))
6		syl23anc.5	. 2 ⊢ (𝜑 → 𝜂)
7		syl131anc.6	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁)
8	1, 5, 6, 7	syl3anc 1371	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 206  df-an 397  df-3an 1089

This theorem is referenced by:  syl132anc  1388  syl231anc  1390  syl133anc  1393  initoeu2lem1  17914  estrres  18041  mulgdir  18922  umgr2edg  28220  2pthfrgr  29291  omndadd2d  31986  omndadd2rd  31987  submomnd  31988  omndmul2  31990  omndmul3  31991  ogrpinv0le  31993  ogrpsub  31994  ogrpaddltbi  31996  ogrpaddltrd  31997  ogrpinv0lt  32000  isarchi3  32093  archirngz  32095  archiabllem1a  32097  archiabllem1b  32098  archiabllem2a  32100  archiabllem2c  32101  orngsqr  32170  ornglmulle  32171  orngrmulle  32172  ofldchr  32180  lineext  34737  brsegle2  34770  cvrcmp  37818  cvrcmp2  37819  atcvreq0  37849  cvlatexch3  37873  cvlcvr1  37874  cvlsupr2  37878  cvlsupr7  37883  atnlej1  37915  atnlej2  37916  cvrval3  37949  ltltncvr  37959  atcvrneN  37966  atcvrj2b  37968  atbtwnex  37984  3noncolr2  37985  3noncolr1N  37986  4noncolr3  37989  3dimlem2  37995  3dimlem3a  37996  3dimlem3  37997  3dimlem3OLDN  37998  3dimlem4a  37999  3dimlem4  38000  3dimlem4OLDN  38001  ps-1  38013  hlatexch4  38017  3atlem1  38019  3atlem2  38020  3atlem3  38021  3atlem4  38022  3atlem5  38023  3atlem6  38024  3atlem7  38025  2llnmat  38060  ps-2c  38064  lplnri3N  38091  lplnexllnN  38100  2llnmeqat  38107  4atlem0a  38129  4atlem0ae  38130  4atlem0be  38131  4atlem9  38139  4atlem10a  38140  4atlem10b  38141  4atlem10  38142  4atlem11a  38143  4atlem11  38145  4atlem12a  38146  dalemcnes  38186  dalempnes  38187  dalemqnet  38188  dalem1  38195  dalemdea  38198  dalem3  38200  dalem5  38203  dalem-cly  38207  dalem27  38235  dalem28  38236  dalem41  38249  dalem45  38253  dalem48  38256  lneq2at  38314  2lnat  38320  2llnma1  38323  2llnma3r  38324  2llnma2  38325  cdlemblem  38329  paddasslem2  38357  pmodl42N  38387  hlmod1i  38392  atmod1i1m  38394  atmod2i1  38397  atmod2i2  38398  atmod3i1  38400  llnexchb2lem  38404  dalawlem2  38408  dalawlem3  38409  dalawlem6  38412  dalawlem7  38413  dalawlem11  38417  dalawlem12  38418  pexmidlem3N  38508  lhpexle3lem  38547  lhpmcvr3  38561  lhp2at0  38568  lhpelim  38573  lhpmod2i2  38574  lhpmod6i1  38575  4atexlempns  38598  4atexlemunv  38602  4atexlemc  38605  4atexlemnclw  38606  4atexlemex2  38607  4atexlemex6  38610  4atex  38612  4atex3  38617  trljat1  38702  trljat2  38703  ltrnatlw  38719  trlval4  38724  cdlemc1  38727  cdlemc3  38729  cdlemc6  38732  cdlemd3  38736  cdlemd4  38737  cdlemd5  38738  cdlemd6  38739  cdlemd7  38740  cdleme00a  38745  cdleme0cp  38750  cdleme0cq  38751  cdleme0e  38753  cdleme02N  38758  cdleme0ex2N  38760  cdleme0moN  38761  cdleme1  38763  cdleme2  38764  cdleme3e  38768  cdleme3g  38770  cdleme3h  38771  cdleme4  38774  cdleme5  38776  cdleme7aa  38778  cdleme7c  38781  cdleme7d  38782  cdleme7e  38783  cdleme8  38786  cdleme9  38789  cdleme10  38790  cdleme16aN  38795  cdleme11a  38796  cdleme11c  38797  cdleme11dN  38798  cdleme11e  38799  cdleme11g  38801  cdleme11h  38802  cdleme11j  38803  cdleme11k  38804  cdleme12  38807  cdleme15a  38810  cdleme15b  38811  cdleme16b  38815  cdleme17c  38824  cdleme0nex  38826  cdleme18d  38831  cdlemednpq  38835  cdleme20zN  38837  cdleme20y  38838  cdleme19a  38839  cdleme19d  38842  cdleme20aN  38845  cdleme20c  38847  cdleme20i  38853  cdleme20j  38854  cdleme21a  38861  cdleme21b  38862  cdleme21c  38863  cdleme21ct  38865  cdleme22cN  38878  cdleme22d  38879  cdleme22e  38880  cdleme22eALTN  38881  cdleme22f  38882  cdleme22f2  38883  cdleme22g  38884  cdleme23c  38887  cdleme41sn3a  38969  cdleme32le  38983  cdleme35b  38986  cdleme35c  38987  cdleme35d  38988  cdleme35e  38989  cdleme36a  38996  cdleme37m  38998  cdleme39a  39001  cdleme42a  39007  cdleme17d2  39031  cdlemeg46frv  39061  cdlemeg46rgv  39064  cdlemf1  39097  cdlemg2fv2  39136  cdlemg2l  39139  cdlemg2m  39140  cdlemg4d  39149  cdlemg4e  39150  cdlemg4f  39151  cdlemg4  39153  cdlemg6c  39156  cdlemg9a  39168  cdlemg10bALTN  39172  cdlemg12a  39179  cdlemg13  39188  cdlemg14f  39189  cdlemg14g  39190  cdlemg17i  39205  cdlemg17pq  39208  cdlemg19  39220  cdlemg21  39222  cdlemg27b  39232  cdlemg33c  39244  cdlemg33d  39245  trlcoabs2N  39258  cdlemg43  39266  cdlemg44b  39268  cdlemg44  39269  cdlemh1  39351  cdlemh2  39352  cdlemi1  39354  tendo0mul  39362  tendo0mulr  39363  cdlemk4  39370  cdlemk9  39375  cdlemk9bN  39376  cdlemk14  39390  cdlemkfid1N  39457  cdlemkid1  39458  cdlemk35s-id  39474  cdlemk39s-id  39476  cdlemk55a  39495  cdlemk55u  39502  cdlemk39u  39504  cdlemk19u  39506  cdlemk56  39507  cdleml8  39519  dia2dimlem1  39600  dia2dimlem2  39601  dia2dimlem3  39602  cdlemn10  39742  dihjust  39753  dihord1  39754  dihlsscpre  39770  dihvalcqpre  39771  dihglbcpreN  39836  dihmeetlem5  39844  dihmeetlem7N  39846  dihjatc1  39847  lincreslvec3  46683  isldepslvec2  46686