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  18109  estrres  18233  mulgdir  19235  omndadd2d  20263  omndadd2rd  20264  submomnd  20265  omndmul2  20266  omndmul3  20267  ogrpinv0le  20269  ogrpsub  20270  ogrpaddltbi  20272  ogrpaddltrd  20273  ogrpinv0lt  20276  orngsqr  21038  ornglmulle  21039  orngrmulle  21040  ofldchr  21795  umgr2edg  29677  2pthfrgr  30772  isarchi3  33635  archirngz  33637  archiabllem1a  33639  archiabllem1b  33640  archiabllem2a  33642  archiabllem2c  33643  lineext  36664  brsegle2  36697  cvrcmp  40164  cvrcmp2  40165  atcvreq0  40195  cvlatexch3  40219  cvlcvr1  40220  cvlsupr2  40224  cvlsupr7  40229  atnlej1  40260  atnlej2  40261  cvrval3  40294  ltltncvr  40304  atcvrneN  40311  atcvrj2b  40313  atbtwnex  40329  3noncolr2  40330  3noncolr1N  40331  4noncolr3  40334  3dimlem2  40340  3dimlem3a  40341  3dimlem3  40342  3dimlem3OLDN  40343  3dimlem4a  40344  3dimlem4  40345  3dimlem4OLDN  40346  ps-1  40358  hlatexch4  40362  3atlem1  40364  3atlem2  40365  3atlem3  40366  3atlem4  40367  3atlem5  40368  3atlem6  40369  3atlem7  40370  2llnmat  40405  ps-2c  40409  lplnri3N  40436  lplnexllnN  40445  2llnmeqat  40452  4atlem0a  40474  4atlem0ae  40475  4atlem0be  40476  4atlem9  40484  4atlem10a  40485  4atlem10b  40486  4atlem10  40487  4atlem11a  40488  4atlem11  40490  4atlem12a  40491  dalemcnes  40531  dalempnes  40532  dalemqnet  40533  dalem1  40540  dalemdea  40543  dalem3  40545  dalem5  40548  dalem-cly  40552  dalem27  40580  dalem28  40581  dalem41  40594  dalem45  40598  dalem48  40601  lneq2at  40659  2lnat  40665  2llnma1  40668  2llnma3r  40669  2llnma2  40670  cdlemblem  40674  paddasslem2  40702  pmodl42N  40732  hlmod1i  40737  atmod1i1m  40739  atmod2i1  40742  atmod2i2  40743  atmod3i1  40745  llnexchb2lem  40749  dalawlem2  40753  dalawlem3  40754  dalawlem6  40757  dalawlem7  40758  dalawlem11  40762  dalawlem12  40763  pexmidlem3N  40853  lhpexle3lem  40892  lhpmcvr3  40906  lhp2at0  40913  lhpelim  40918  lhpmod2i2  40919  lhpmod6i1  40920  4atexlempns  40943  4atexlemunv  40947  4atexlemc  40950  4atexlemnclw  40951  4atexlemex2  40952  4atexlemex6  40955  4atex  40957  4atex3  40962  trljat1  41047  trljat2  41048  ltrnatlw  41064  trlval4  41069  cdlemc1  41072  cdlemc3  41074  cdlemc6  41077  cdlemd3  41081  cdlemd4  41082  cdlemd5  41083  cdlemd6  41084  cdlemd7  41085  cdleme00a  41090  cdleme0cp  41095  cdleme0cq  41096  cdleme0e  41098  cdleme02N  41103  cdleme0ex2N  41105  cdleme0moN  41106  cdleme1  41108  cdleme2  41109  cdleme3e  41113  cdleme3g  41115  cdleme3h  41116  cdleme4  41119  cdleme5  41121  cdleme7aa  41123  cdleme7c  41126  cdleme7d  41127  cdleme7e  41128  cdleme8  41131  cdleme9  41134  cdleme10  41135  cdleme16aN  41140  cdleme11a  41141  cdleme11c  41142  cdleme11dN  41143  cdleme11e  41144  cdleme11g  41146  cdleme11h  41147  cdleme11j  41148  cdleme11k  41149  cdleme12  41152  cdleme15a  41155  cdleme15b  41156  cdleme16b  41160  cdleme17c  41169  cdleme0nex  41171  cdleme18d  41176  cdlemednpq  41180  cdleme20zN  41182  cdleme20y  41183  cdleme19a  41184  cdleme19d  41187  cdleme20aN  41190  cdleme20c  41192  cdleme20i  41198  cdleme20j  41199  cdleme21a  41206  cdleme21b  41207  cdleme21c  41208  cdleme21ct  41210  cdleme22cN  41223  cdleme22d  41224  cdleme22e  41225  cdleme22eALTN  41226  cdleme22f  41227  cdleme22f2  41228  cdleme22g  41229  cdleme23c  41232  cdleme41sn3a  41314  cdleme32le  41328  cdleme35b  41331  cdleme35c  41332  cdleme35d  41333  cdleme35e  41334  cdleme36a  41341  cdleme37m  41343  cdleme39a  41346  cdleme42a  41352  cdleme17d2  41376  cdlemeg46frv  41406  cdlemeg46rgv  41409  cdlemf1  41442  cdlemg2fv2  41481  cdlemg2l  41484  cdlemg2m  41485  cdlemg4d  41494  cdlemg4e  41495  cdlemg4f  41496  cdlemg4  41498  cdlemg6c  41501  cdlemg9a  41513  cdlemg10bALTN  41517  cdlemg12a  41524  cdlemg13  41533  cdlemg14f  41534  cdlemg14g  41535  cdlemg17i  41550  cdlemg17pq  41553  cdlemg19  41565  cdlemg21  41567  cdlemg27b  41577  cdlemg33c  41589  cdlemg33d  41590  trlcoabs2N  41603  cdlemg43  41611  cdlemg44b  41613  cdlemg44  41614  cdlemh1  41696  cdlemh2  41697  cdlemi1  41699  tendo0mul  41707  tendo0mulr  41708  cdlemk4  41715  cdlemk9  41720  cdlemk9bN  41721  cdlemk14  41735  cdlemkfid1N  41802  cdlemkid1  41803  cdlemk35s-id  41819  cdlemk39s-id  41821  cdlemk55a  41840  cdlemk55u  41847  cdlemk39u  41849  cdlemk19u  41851  cdlemk56  41852  cdleml8  41864  dia2dimlem1  41945  dia2dimlem2  41946  dia2dimlem3  41947  cdlemn10  42087  dihjust  42098  dihord1  42099  dihlsscpre  42115  dihvalcqpre  42116  dihglbcpreN  42181  dihmeetlem5  42189  dihmeetlem7N  42191  dihjatc1  42192  modmknepk  48264  modm2nep1  48268  modp2nep1  48269  modm1nep2  48270  modm1nem2  48271  lincreslvec3  49420  isldepslvec2  49423