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  17277  estrres  17392  mulgdir  18262  umgr2edg  26994  2pthfrgr  28066  omndadd2d  30713  omndadd2rd  30714  submomnd  30715  omndmul2  30717  omndmul3  30718  ogrpinv0le  30720  ogrpsub  30721  ogrpaddltbi  30723  ogrpaddltrd  30724  ogrpinv0lt  30727  isarchi3  30820  archirngz  30822  archiabllem1a  30824  archiabllem1b  30825  archiabllem2a  30827  archiabllem2c  30828  orngsqr  30881  ornglmulle  30882  orngrmulle  30883  ofldchr  30891  lineext  33541  brsegle2  33574  cvrcmp  36423  cvrcmp2  36424  atcvreq0  36454  cvlatexch3  36478  cvlcvr1  36479  cvlsupr2  36483  cvlsupr7  36488  atnlej1  36519  atnlej2  36520  cvrval3  36553  ltltncvr  36563  atcvrneN  36570  atcvrj2b  36572  atbtwnex  36588  3noncolr2  36589  3noncolr1N  36590  4noncolr3  36593  3dimlem2  36599  3dimlem3a  36600  3dimlem3  36601  3dimlem3OLDN  36602  3dimlem4a  36603  3dimlem4  36604  3dimlem4OLDN  36605  ps-1  36617  hlatexch4  36621  3atlem1  36623  3atlem2  36624  3atlem3  36625  3atlem4  36626  3atlem5  36627  3atlem6  36628  3atlem7  36629  2llnmat  36664  ps-2c  36668  lplnri3N  36695  lplnexllnN  36704  2llnmeqat  36711  4atlem0a  36733  4atlem0ae  36734  4atlem0be  36735  4atlem9  36743  4atlem10a  36744  4atlem10b  36745  4atlem10  36746  4atlem11a  36747  4atlem11  36749  4atlem12a  36750  dalemcnes  36790  dalempnes  36791  dalemqnet  36792  dalem1  36799  dalemdea  36802  dalem3  36804  dalem5  36807  dalem-cly  36811  dalem27  36839  dalem28  36840  dalem41  36853  dalem45  36857  dalem48  36860  lneq2at  36918  2lnat  36924  2llnma1  36927  2llnma3r  36928  2llnma2  36929  cdlemblem  36933  paddasslem2  36961  pmodl42N  36991  hlmod1i  36996  atmod1i1m  36998  atmod2i1  37001  atmod2i2  37002  atmod3i1  37004  llnexchb2lem  37008  dalawlem2  37012  dalawlem3  37013  dalawlem6  37016  dalawlem7  37017  dalawlem11  37021  dalawlem12  37022  pexmidlem3N  37112  lhpexle3lem  37151  lhpmcvr3  37165  lhp2at0  37172  lhpelim  37177  lhpmod2i2  37178  lhpmod6i1  37179  4atexlempns  37202  4atexlemunv  37206  4atexlemc  37209  4atexlemnclw  37210  4atexlemex2  37211  4atexlemex6  37214  4atex  37216  4atex3  37221  trljat1  37306  trljat2  37307  ltrnatlw  37323  trlval4  37328  cdlemc1  37331  cdlemc3  37333  cdlemc6  37336  cdlemd3  37340  cdlemd4  37341  cdlemd5  37342  cdlemd6  37343  cdlemd7  37344  cdleme00a  37349  cdleme0cp  37354  cdleme0cq  37355  cdleme0e  37357  cdleme02N  37362  cdleme0ex2N  37364  cdleme0moN  37365  cdleme1  37367  cdleme2  37368  cdleme3e  37372  cdleme3g  37374  cdleme3h  37375  cdleme4  37378  cdleme5  37380  cdleme7aa  37382  cdleme7c  37385  cdleme7d  37386  cdleme7e  37387  cdleme8  37390  cdleme9  37393  cdleme10  37394  cdleme16aN  37399  cdleme11a  37400  cdleme11c  37401  cdleme11dN  37402  cdleme11e  37403  cdleme11g  37405  cdleme11h  37406  cdleme11j  37407  cdleme11k  37408  cdleme12  37411  cdleme15a  37414  cdleme15b  37415  cdleme16b  37419  cdleme17c  37428  cdleme0nex  37430  cdleme18d  37435  cdlemednpq  37439  cdleme20zN  37441  cdleme20y  37442  cdleme19a  37443  cdleme19d  37446  cdleme20aN  37449  cdleme20c  37451  cdleme20i  37457  cdleme20j  37458  cdleme21a  37465  cdleme21b  37466  cdleme21c  37467  cdleme21ct  37469  cdleme22cN  37482  cdleme22d  37483  cdleme22e  37484  cdleme22eALTN  37485  cdleme22f  37486  cdleme22f2  37487  cdleme22g  37488  cdleme23c  37491  cdleme41sn3a  37573  cdleme32le  37587  cdleme35b  37590  cdleme35c  37591  cdleme35d  37592  cdleme35e  37593  cdleme36a  37600  cdleme37m  37602  cdleme39a  37605  cdleme42a  37611  cdleme17d2  37635  cdlemeg46frv  37665  cdlemeg46rgv  37668  cdlemf1  37701  cdlemg2fv2  37740  cdlemg2l  37743  cdlemg2m  37744  cdlemg4d  37753  cdlemg4e  37754  cdlemg4f  37755  cdlemg4  37757  cdlemg6c  37760  cdlemg9a  37772  cdlemg10bALTN  37776  cdlemg12a  37783  cdlemg13  37792  cdlemg14f  37793  cdlemg14g  37794  cdlemg17i  37809  cdlemg17pq  37812  cdlemg19  37824  cdlemg21  37826  cdlemg27b  37836  cdlemg33c  37848  cdlemg33d  37849  trlcoabs2N  37862  cdlemg43  37870  cdlemg44b  37872  cdlemg44  37873  cdlemh1  37955  cdlemh2  37956  cdlemi1  37958  tendo0mul  37966  tendo0mulr  37967  cdlemk4  37974  cdlemk9  37979  cdlemk9bN  37980  cdlemk14  37994  cdlemkfid1N  38061  cdlemkid1  38062  cdlemk35s-id  38078  cdlemk39s-id  38080  cdlemk55a  38099  cdlemk55u  38106  cdlemk39u  38108  cdlemk19u  38110  cdlemk56  38111  cdleml8  38123  dia2dimlem1  38204  dia2dimlem2  38205  dia2dimlem3  38206  cdlemn10  38346  dihjust  38357  dihord1  38358  dihlsscpre  38374  dihvalcqpre  38375  dihglbcpreN  38440  dihmeetlem5  38448  dihmeetlem7N  38450  dihjatc1  38451  lincreslvec3  44544  isldepslvec2  44547