Theorem syl131anc 1363

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

Syntax hints:   → wi 4   ∧ w3a 1068

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 199  df-an 388  df-3an 1070

This theorem is referenced by:  syl132anc  1368  syl231anc  1370  syl133anc  1373  initoeu2lem1  17122  estrres  17237  mulgdir  18033  umgr2edg  26684  2pthfrgr  27808  omndadd2d  30405  omndadd2rd  30406  submomnd  30407  omndmul2  30409  omndmul3  30410  ogrpinvOLD  30412  ogrpinv0le  30413  ogrpsub  30414  ogrpaddltbi  30416  ogrpaddltrd  30417  ogrpinv0lt  30420  isarchi3  30438  archirngz  30440  archiabllem1a  30442  archiabllem1b  30443  archiabllem2a  30445  archiabllem2c  30446  orngsqr  30512  ornglmulle  30513  orngrmulle  30514  ofldchr  30522  lineext  32998  brsegle2  33031  cvrcmp  35812  cvrcmp2  35813  atcvreq0  35843  cvlatexch3  35867  cvlcvr1  35868  cvlsupr2  35872  cvlsupr7  35877  atnlej1  35908  atnlej2  35909  cvrval3  35942  ltltncvr  35952  atcvrneN  35959  atcvrj2b  35961  atbtwnex  35977  3noncolr2  35978  3noncolr1N  35979  4noncolr3  35982  3dimlem2  35988  3dimlem3a  35989  3dimlem3  35990  3dimlem3OLDN  35991  3dimlem4a  35992  3dimlem4  35993  3dimlem4OLDN  35994  ps-1  36006  hlatexch4  36010  3atlem1  36012  3atlem2  36013  3atlem3  36014  3atlem4  36015  3atlem5  36016  3atlem6  36017  3atlem7  36018  2llnmat  36053  ps-2c  36057  lplnri3N  36084  lplnexllnN  36093  2llnmeqat  36100  4atlem0a  36122  4atlem0ae  36123  4atlem0be  36124  4atlem9  36132  4atlem10a  36133  4atlem10b  36134  4atlem10  36135  4atlem11a  36136  4atlem11  36138  4atlem12a  36139  dalemcnes  36179  dalempnes  36180  dalemqnet  36181  dalem1  36188  dalemdea  36191  dalem3  36193  dalem5  36196  dalem-cly  36200  dalem27  36228  dalem28  36229  dalem41  36242  dalem45  36246  dalem48  36249  lneq2at  36307  2lnat  36313  2llnma1  36316  2llnma3r  36317  2llnma2  36318  cdlemblem  36322  paddasslem2  36350  pmodl42N  36380  hlmod1i  36385  atmod1i1m  36387  atmod2i1  36390  atmod2i2  36391  atmod3i1  36393  llnexchb2lem  36397  dalawlem2  36401  dalawlem3  36402  dalawlem6  36405  dalawlem7  36406  dalawlem11  36410  dalawlem12  36411  pexmidlem3N  36501  lhpexle3lem  36540  lhpmcvr3  36554  lhp2at0  36561  lhpelim  36566  lhpmod2i2  36567  lhpmod6i1  36568  4atexlempns  36591  4atexlemunv  36595  4atexlemc  36598  4atexlemnclw  36599  4atexlemex2  36600  4atexlemex6  36603  4atex  36605  4atex3  36610  trljat1  36695  trljat2  36696  ltrnatlw  36712  trlval4  36717  cdlemc1  36720  cdlemc3  36722  cdlemc6  36725  cdlemd3  36729  cdlemd4  36730  cdlemd5  36731  cdlemd6  36732  cdlemd7  36733  cdleme00a  36738  cdleme0cp  36743  cdleme0cq  36744  cdleme0e  36746  cdleme02N  36751  cdleme0ex2N  36753  cdleme0moN  36754  cdleme1  36756  cdleme2  36757  cdleme3e  36761  cdleme3g  36763  cdleme3h  36764  cdleme4  36767  cdleme5  36769  cdleme7aa  36771  cdleme7c  36774  cdleme7d  36775  cdleme7e  36776  cdleme8  36779  cdleme9  36782  cdleme10  36783  cdleme16aN  36788  cdleme11a  36789  cdleme11c  36790  cdleme11dN  36791  cdleme11e  36792  cdleme11g  36794  cdleme11h  36795  cdleme11j  36796  cdleme11k  36797  cdleme12  36800  cdleme15a  36803  cdleme15b  36804  cdleme16b  36808  cdleme17c  36817  cdleme0nex  36819  cdleme18d  36824  cdlemednpq  36828  cdleme20zN  36830  cdleme20y  36831  cdleme19a  36832  cdleme19d  36835  cdleme20aN  36838  cdleme20c  36840  cdleme20i  36846  cdleme20j  36847  cdleme21a  36854  cdleme21b  36855  cdleme21c  36856  cdleme21ct  36858  cdleme22cN  36871  cdleme22d  36872  cdleme22e  36873  cdleme22eALTN  36874  cdleme22f  36875  cdleme22f2  36876  cdleme22g  36877  cdleme23c  36880  cdleme41sn3a  36962  cdleme32le  36976  cdleme35b  36979  cdleme35c  36980  cdleme35d  36981  cdleme35e  36982  cdleme36a  36989  cdleme37m  36991  cdleme39a  36994  cdleme42a  37000  cdleme17d2  37024  cdlemeg46frv  37054  cdlemeg46rgv  37057  cdlemf1  37090  cdlemg2fv2  37129  cdlemg2l  37132  cdlemg2m  37133  cdlemg4d  37142  cdlemg4e  37143  cdlemg4f  37144  cdlemg4  37146  cdlemg6c  37149  cdlemg9a  37161  cdlemg10bALTN  37165  cdlemg12a  37172  cdlemg13  37181  cdlemg14f  37182  cdlemg14g  37183  cdlemg17i  37198  cdlemg17pq  37201  cdlemg19  37213  cdlemg21  37215  cdlemg27b  37225  cdlemg33c  37237  cdlemg33d  37238  trlcoabs2N  37251  cdlemg43  37259  cdlemg44b  37261  cdlemg44  37262  cdlemh1  37344  cdlemh2  37345  cdlemi1  37347  tendo0mul  37355  tendo0mulr  37356  cdlemk4  37363  cdlemk9  37368  cdlemk9bN  37369  cdlemk14  37383  cdlemkfid1N  37450  cdlemkid1  37451  cdlemk35s-id  37467  cdlemk39s-id  37469  cdlemk55a  37488  cdlemk55u  37495  cdlemk39u  37497  cdlemk19u  37499  cdlemk56  37500  cdleml8  37512  dia2dimlem1  37593  dia2dimlem2  37594  dia2dimlem3  37595  cdlemn10  37735  dihjust  37746  dihord1  37747  dihlsscpre  37763  dihvalcqpre  37764  dihglbcpreN  37829  dihmeetlem5  37837  dihmeetlem7N  37839  dihjatc1  37840  lincreslvec3  43844  isldepslvec2  43847