Theorem syl131anc 1379

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 399  df-3an 1085

This theorem is referenced by:  syl132anc  1384  syl231anc  1386  syl133anc  1389  initoeu2lem1  17274  estrres  17389  mulgdir  18259  umgr2edg  26991  2pthfrgr  28063  omndadd2d  30709  omndadd2rd  30710  submomnd  30711  omndmul2  30713  omndmul3  30714  ogrpinv0le  30716  ogrpsub  30717  ogrpaddltbi  30719  ogrpaddltrd  30720  ogrpinv0lt  30723  isarchi3  30816  archirngz  30818  archiabllem1a  30820  archiabllem1b  30821  archiabllem2a  30823  archiabllem2c  30824  orngsqr  30877  ornglmulle  30878  orngrmulle  30879  ofldchr  30887  lineext  33537  brsegle2  33570  cvrcmp  36434  cvrcmp2  36435  atcvreq0  36465  cvlatexch3  36489  cvlcvr1  36490  cvlsupr2  36494  cvlsupr7  36499  atnlej1  36530  atnlej2  36531  cvrval3  36564  ltltncvr  36574  atcvrneN  36581  atcvrj2b  36583  atbtwnex  36599  3noncolr2  36600  3noncolr1N  36601  4noncolr3  36604  3dimlem2  36610  3dimlem3a  36611  3dimlem3  36612  3dimlem3OLDN  36613  3dimlem4a  36614  3dimlem4  36615  3dimlem4OLDN  36616  ps-1  36628  hlatexch4  36632  3atlem1  36634  3atlem2  36635  3atlem3  36636  3atlem4  36637  3atlem5  36638  3atlem6  36639  3atlem7  36640  2llnmat  36675  ps-2c  36679  lplnri3N  36706  lplnexllnN  36715  2llnmeqat  36722  4atlem0a  36744  4atlem0ae  36745  4atlem0be  36746  4atlem9  36754  4atlem10a  36755  4atlem10b  36756  4atlem10  36757  4atlem11a  36758  4atlem11  36760  4atlem12a  36761  dalemcnes  36801  dalempnes  36802  dalemqnet  36803  dalem1  36810  dalemdea  36813  dalem3  36815  dalem5  36818  dalem-cly  36822  dalem27  36850  dalem28  36851  dalem41  36864  dalem45  36868  dalem48  36871  lneq2at  36929  2lnat  36935  2llnma1  36938  2llnma3r  36939  2llnma2  36940  cdlemblem  36944  paddasslem2  36972  pmodl42N  37002  hlmod1i  37007  atmod1i1m  37009  atmod2i1  37012  atmod2i2  37013  atmod3i1  37015  llnexchb2lem  37019  dalawlem2  37023  dalawlem3  37024  dalawlem6  37027  dalawlem7  37028  dalawlem11  37032  dalawlem12  37033  pexmidlem3N  37123  lhpexle3lem  37162  lhpmcvr3  37176  lhp2at0  37183  lhpelim  37188  lhpmod2i2  37189  lhpmod6i1  37190  4atexlempns  37213  4atexlemunv  37217  4atexlemc  37220  4atexlemnclw  37221  4atexlemex2  37222  4atexlemex6  37225  4atex  37227  4atex3  37232  trljat1  37317  trljat2  37318  ltrnatlw  37334  trlval4  37339  cdlemc1  37342  cdlemc3  37344  cdlemc6  37347  cdlemd3  37351  cdlemd4  37352  cdlemd5  37353  cdlemd6  37354  cdlemd7  37355  cdleme00a  37360  cdleme0cp  37365  cdleme0cq  37366  cdleme0e  37368  cdleme02N  37373  cdleme0ex2N  37375  cdleme0moN  37376  cdleme1  37378  cdleme2  37379  cdleme3e  37383  cdleme3g  37385  cdleme3h  37386  cdleme4  37389  cdleme5  37391  cdleme7aa  37393  cdleme7c  37396  cdleme7d  37397  cdleme7e  37398  cdleme8  37401  cdleme9  37404  cdleme10  37405  cdleme16aN  37410  cdleme11a  37411  cdleme11c  37412  cdleme11dN  37413  cdleme11e  37414  cdleme11g  37416  cdleme11h  37417  cdleme11j  37418  cdleme11k  37419  cdleme12  37422  cdleme15a  37425  cdleme15b  37426  cdleme16b  37430  cdleme17c  37439  cdleme0nex  37441  cdleme18d  37446  cdlemednpq  37450  cdleme20zN  37452  cdleme20y  37453  cdleme19a  37454  cdleme19d  37457  cdleme20aN  37460  cdleme20c  37462  cdleme20i  37468  cdleme20j  37469  cdleme21a  37476  cdleme21b  37477  cdleme21c  37478  cdleme21ct  37480  cdleme22cN  37493  cdleme22d  37494  cdleme22e  37495  cdleme22eALTN  37496  cdleme22f  37497  cdleme22f2  37498  cdleme22g  37499  cdleme23c  37502  cdleme41sn3a  37584  cdleme32le  37598  cdleme35b  37601  cdleme35c  37602  cdleme35d  37603  cdleme35e  37604  cdleme36a  37611  cdleme37m  37613  cdleme39a  37616  cdleme42a  37622  cdleme17d2  37646  cdlemeg46frv  37676  cdlemeg46rgv  37679  cdlemf1  37712  cdlemg2fv2  37751  cdlemg2l  37754  cdlemg2m  37755  cdlemg4d  37764  cdlemg4e  37765  cdlemg4f  37766  cdlemg4  37768  cdlemg6c  37771  cdlemg9a  37783  cdlemg10bALTN  37787  cdlemg12a  37794  cdlemg13  37803  cdlemg14f  37804  cdlemg14g  37805  cdlemg17i  37820  cdlemg17pq  37823  cdlemg19  37835  cdlemg21  37837  cdlemg27b  37847  cdlemg33c  37859  cdlemg33d  37860  trlcoabs2N  37873  cdlemg43  37881  cdlemg44b  37883  cdlemg44  37884  cdlemh1  37966  cdlemh2  37967  cdlemi1  37969  tendo0mul  37977  tendo0mulr  37978  cdlemk4  37985  cdlemk9  37990  cdlemk9bN  37991  cdlemk14  38005  cdlemkfid1N  38072  cdlemkid1  38073  cdlemk35s-id  38089  cdlemk39s-id  38091  cdlemk55a  38110  cdlemk55u  38117  cdlemk39u  38119  cdlemk19u  38121  cdlemk56  38122  cdleml8  38134  dia2dimlem1  38215  dia2dimlem2  38216  dia2dimlem3  38217  cdlemn10  38357  dihjust  38368  dihord1  38369  dihlsscpre  38385  dihvalcqpre  38386  dihglbcpreN  38451  dihmeetlem5  38459  dihmeetlem7N  38461  dihjatc1  38462  lincreslvec3  44557  isldepslvec2  44560