Theorem syl131anc 1410

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  syl132anc  1415  syl231anc  1417  syl133anc  1420  initoeu2lem1  18194  estrres  18318  mulgdir  19321  omndadd2d  20349  omndadd2rd  20350  submomnd  20351  omndmul2  20352  omndmul3  20353  ogrpinv0le  20355  ogrpsub  20356  ogrpaddltbi  20358  ogrpaddltrd  20359  ogrpinv0lt  20362  orngsqr  21128  ornglmulle  21129  orngrmulle  21130  ofldchr  21887  umgr2edg  29795  2pthfrgr  30890  isarchi3  33794  archirngz  33796  archiabllem1a  33798  archiabllem1b  33799  archiabllem2a  33801  archiabllem2c  33802  lineext  36933  brsegle2  36966  cvrcmp  40433  cvrcmp2  40434  atcvreq0  40464  cvlatexch3  40488  cvlcvr1  40489  cvlsupr2  40493  cvlsupr7  40498  atnlej1  40529  atnlej2  40530  cvrval3  40563  ltltncvr  40573  atcvrneN  40580  atcvrj2b  40582  atbtwnex  40598  3noncolr2  40599  3noncolr1N  40600  4noncolr3  40603  3dimlem2  40609  3dimlem3a  40610  3dimlem3  40611  3dimlem3OLDN  40612  3dimlem4a  40613  3dimlem4  40614  3dimlem4OLDN  40615  ps-1  40627  hlatexch4  40631  3atlem1  40633  3atlem2  40634  3atlem3  40635  3atlem4  40636  3atlem5  40637  3atlem6  40638  3atlem7  40639  2llnmat  40674  ps-2c  40678  lplnri3N  40705  lplnexllnN  40714  2llnmeqat  40721  4atlem0a  40743  4atlem0ae  40744  4atlem0be  40745  4atlem9  40753  4atlem10a  40754  4atlem10b  40755  4atlem10  40756  4atlem11a  40757  4atlem11  40759  4atlem12a  40760  dalemcnes  40800  dalempnes  40801  dalemqnet  40802  dalem1  40809  dalemdea  40812  dalem3  40814  dalem5  40817  dalem-cly  40821  dalem27  40849  dalem28  40850  dalem41  40863  dalem45  40867  dalem48  40870  lneq2at  40928  2lnat  40934  2llnma1  40937  2llnma3r  40938  2llnma2  40939  cdlemblem  40943  paddasslem2  40971  pmodl42N  41001  hlmod1i  41006  atmod1i1m  41008  atmod2i1  41011  atmod2i2  41012  atmod3i1  41014  llnexchb2lem  41018  dalawlem2  41022  dalawlem3  41023  dalawlem6  41026  dalawlem7  41027  dalawlem11  41031  dalawlem12  41032  pexmidlem3N  41122  lhpexle3lem  41161  lhpmcvr3  41175  lhp2at0  41182  lhpelim  41187  lhpmod2i2  41188  lhpmod6i1  41189  4atexlempns  41212  4atexlemunv  41216  4atexlemc  41219  4atexlemnclw  41220  4atexlemex2  41221  4atexlemex6  41224  4atex  41226  4atex3  41231  trljat1  41316  trljat2  41317  ltrnatlw  41333  trlval4  41338  cdlemc1  41341  cdlemc3  41343  cdlemc6  41346  cdlemd3  41350  cdlemd4  41351  cdlemd5  41352  cdlemd6  41353  cdlemd7  41354  cdleme00a  41359  cdleme0cp  41364  cdleme0cq  41365  cdleme0e  41367  cdleme02N  41372  cdleme0ex2N  41374  cdleme0moN  41375  cdleme1  41377  cdleme2  41378  cdleme3e  41382  cdleme3g  41384  cdleme3h  41385  cdleme4  41388  cdleme5  41390  cdleme7aa  41392  cdleme7c  41395  cdleme7d  41396  cdleme7e  41397  cdleme8  41400  cdleme9  41403  cdleme10  41404  cdleme16aN  41409  cdleme11a  41410  cdleme11c  41411  cdleme11dN  41412  cdleme11e  41413  cdleme11g  41415  cdleme11h  41416  cdleme11j  41417  cdleme11k  41418  cdleme12  41421  cdleme15a  41424  cdleme15b  41425  cdleme16b  41429  cdleme17c  41438  cdleme0nex  41440  cdleme18d  41445  cdlemednpq  41449  cdleme20zN  41451  cdleme20y  41452  cdleme19a  41453  cdleme19d  41456  cdleme20aN  41459  cdleme20c  41461  cdleme20i  41467  cdleme20j  41468  cdleme21a  41475  cdleme21b  41476  cdleme21c  41477  cdleme21ct  41479  cdleme22cN  41492  cdleme22d  41493  cdleme22e  41494  cdleme22eALTN  41495  cdleme22f  41496  cdleme22f2  41497  cdleme22g  41498  cdleme23c  41501  cdleme41sn3a  41583  cdleme32le  41597  cdleme35b  41600  cdleme35c  41601  cdleme35d  41602  cdleme35e  41603  cdleme36a  41610  cdleme37m  41612  cdleme39a  41615  cdleme42a  41621  cdleme17d2  41645  cdlemeg46frv  41675  cdlemeg46rgv  41678  cdlemf1  41711  cdlemg2fv2  41750  cdlemg2l  41753  cdlemg2m  41754  cdlemg4d  41763  cdlemg4e  41764  cdlemg4f  41765  cdlemg4  41767  cdlemg6c  41770  cdlemg9a  41782  cdlemg10bALTN  41786  cdlemg12a  41793  cdlemg13  41802  cdlemg14f  41803  cdlemg14g  41804  cdlemg17i  41819  cdlemg17pq  41822  cdlemg19  41834  cdlemg21  41836  cdlemg27b  41846  cdlemg33c  41858  cdlemg33d  41859  trlcoabs2N  41872  cdlemg43  41880  cdlemg44b  41882  cdlemg44  41883  cdlemh1  41965  cdlemh2  41966  cdlemi1  41968  tendo0mul  41976  tendo0mulr  41977  cdlemk4  41984  cdlemk9  41989  cdlemk9bN  41990  cdlemk14  42004  cdlemkfid1N  42071  cdlemkid1  42072  cdlemk35s-id  42088  cdlemk39s-id  42090  cdlemk55a  42109  cdlemk55u  42116  cdlemk39u  42118  cdlemk19u  42120  cdlemk56  42121  cdleml8  42133  dia2dimlem1  42214  dia2dimlem2  42215  dia2dimlem3  42216  cdlemn10  42356  dihjust  42367  dihord1  42368  dihlsscpre  42384  dihvalcqpre  42385  dihglbcpreN  42450  dihmeetlem5  42458  dihmeetlem7N  42460  dihjatc1  42461  modmknepk  48531  modm2nep1  48535  modp2nep1  48536  modm1nep2  48537  modm1nem2  48538  lincreslvec3  49687  isldepslvec2  49690