Theorem syl131anc 1381

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 395  df-3an 1087

This theorem is referenced by:  syl132anc  1386  syl231anc  1388  syl133anc  1391  initoeu2lem1  17968  estrres  18095  mulgdir  19022  umgr2edg  28733  2pthfrgr  29804  omndadd2d  32496  omndadd2rd  32497  submomnd  32498  omndmul2  32500  omndmul3  32501  ogrpinv0le  32503  ogrpsub  32504  ogrpaddltbi  32506  ogrpaddltrd  32507  ogrpinv0lt  32510  isarchi3  32603  archirngz  32605  archiabllem1a  32607  archiabllem1b  32608  archiabllem2a  32610  archiabllem2c  32611  orngsqr  32692  ornglmulle  32693  orngrmulle  32694  ofldchr  32702  lineext  35352  brsegle2  35385  cvrcmp  38456  cvrcmp2  38457  atcvreq0  38487  cvlatexch3  38511  cvlcvr1  38512  cvlsupr2  38516  cvlsupr7  38521  atnlej1  38553  atnlej2  38554  cvrval3  38587  ltltncvr  38597  atcvrneN  38604  atcvrj2b  38606  atbtwnex  38622  3noncolr2  38623  3noncolr1N  38624  4noncolr3  38627  3dimlem2  38633  3dimlem3a  38634  3dimlem3  38635  3dimlem3OLDN  38636  3dimlem4a  38637  3dimlem4  38638  3dimlem4OLDN  38639  ps-1  38651  hlatexch4  38655  3atlem1  38657  3atlem2  38658  3atlem3  38659  3atlem4  38660  3atlem5  38661  3atlem6  38662  3atlem7  38663  2llnmat  38698  ps-2c  38702  lplnri3N  38729  lplnexllnN  38738  2llnmeqat  38745  4atlem0a  38767  4atlem0ae  38768  4atlem0be  38769  4atlem9  38777  4atlem10a  38778  4atlem10b  38779  4atlem10  38780  4atlem11a  38781  4atlem11  38783  4atlem12a  38784  dalemcnes  38824  dalempnes  38825  dalemqnet  38826  dalem1  38833  dalemdea  38836  dalem3  38838  dalem5  38841  dalem-cly  38845  dalem27  38873  dalem28  38874  dalem41  38887  dalem45  38891  dalem48  38894  lneq2at  38952  2lnat  38958  2llnma1  38961  2llnma3r  38962  2llnma2  38963  cdlemblem  38967  paddasslem2  38995  pmodl42N  39025  hlmod1i  39030  atmod1i1m  39032  atmod2i1  39035  atmod2i2  39036  atmod3i1  39038  llnexchb2lem  39042  dalawlem2  39046  dalawlem3  39047  dalawlem6  39050  dalawlem7  39051  dalawlem11  39055  dalawlem12  39056  pexmidlem3N  39146  lhpexle3lem  39185  lhpmcvr3  39199  lhp2at0  39206  lhpelim  39211  lhpmod2i2  39212  lhpmod6i1  39213  4atexlempns  39236  4atexlemunv  39240  4atexlemc  39243  4atexlemnclw  39244  4atexlemex2  39245  4atexlemex6  39248  4atex  39250  4atex3  39255  trljat1  39340  trljat2  39341  ltrnatlw  39357  trlval4  39362  cdlemc1  39365  cdlemc3  39367  cdlemc6  39370  cdlemd3  39374  cdlemd4  39375  cdlemd5  39376  cdlemd6  39377  cdlemd7  39378  cdleme00a  39383  cdleme0cp  39388  cdleme0cq  39389  cdleme0e  39391  cdleme02N  39396  cdleme0ex2N  39398  cdleme0moN  39399  cdleme1  39401  cdleme2  39402  cdleme3e  39406  cdleme3g  39408  cdleme3h  39409  cdleme4  39412  cdleme5  39414  cdleme7aa  39416  cdleme7c  39419  cdleme7d  39420  cdleme7e  39421  cdleme8  39424  cdleme9  39427  cdleme10  39428  cdleme16aN  39433  cdleme11a  39434  cdleme11c  39435  cdleme11dN  39436  cdleme11e  39437  cdleme11g  39439  cdleme11h  39440  cdleme11j  39441  cdleme11k  39442  cdleme12  39445  cdleme15a  39448  cdleme15b  39449  cdleme16b  39453  cdleme17c  39462  cdleme0nex  39464  cdleme18d  39469  cdlemednpq  39473  cdleme20zN  39475  cdleme20y  39476  cdleme19a  39477  cdleme19d  39480  cdleme20aN  39483  cdleme20c  39485  cdleme20i  39491  cdleme20j  39492  cdleme21a  39499  cdleme21b  39500  cdleme21c  39501  cdleme21ct  39503  cdleme22cN  39516  cdleme22d  39517  cdleme22e  39518  cdleme22eALTN  39519  cdleme22f  39520  cdleme22f2  39521  cdleme22g  39522  cdleme23c  39525  cdleme41sn3a  39607  cdleme32le  39621  cdleme35b  39624  cdleme35c  39625  cdleme35d  39626  cdleme35e  39627  cdleme36a  39634  cdleme37m  39636  cdleme39a  39639  cdleme42a  39645  cdleme17d2  39669  cdlemeg46frv  39699  cdlemeg46rgv  39702  cdlemf1  39735  cdlemg2fv2  39774  cdlemg2l  39777  cdlemg2m  39778  cdlemg4d  39787  cdlemg4e  39788  cdlemg4f  39789  cdlemg4  39791  cdlemg6c  39794  cdlemg9a  39806  cdlemg10bALTN  39810  cdlemg12a  39817  cdlemg13  39826  cdlemg14f  39827  cdlemg14g  39828  cdlemg17i  39843  cdlemg17pq  39846  cdlemg19  39858  cdlemg21  39860  cdlemg27b  39870  cdlemg33c  39882  cdlemg33d  39883  trlcoabs2N  39896  cdlemg43  39904  cdlemg44b  39906  cdlemg44  39907  cdlemh1  39989  cdlemh2  39990  cdlemi1  39992  tendo0mul  40000  tendo0mulr  40001  cdlemk4  40008  cdlemk9  40013  cdlemk9bN  40014  cdlemk14  40028  cdlemkfid1N  40095  cdlemkid1  40096  cdlemk35s-id  40112  cdlemk39s-id  40114  cdlemk55a  40133  cdlemk55u  40140  cdlemk39u  40142  cdlemk19u  40144  cdlemk56  40145  cdleml8  40157  dia2dimlem1  40238  dia2dimlem2  40239  dia2dimlem3  40240  cdlemn10  40380  dihjust  40391  dihord1  40392  dihlsscpre  40408  dihvalcqpre  40409  dihglbcpreN  40474  dihmeetlem5  40482  dihmeetlem7N  40484  dihjatc1  40485  lincreslvec3  47250  isldepslvec2  47253