Theorem syl131anc 1385

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  syl132anc  1390  syl231anc  1392  syl133anc  1395  initoeu2lem1  17923  estrres  18047  mulgdir  19021  omndadd2d  20044  omndadd2rd  20045  submomnd  20046  omndmul2  20047  omndmul3  20048  ogrpinv0le  20050  ogrpsub  20051  ogrpaddltbi  20053  ogrpaddltrd  20054  ogrpinv0lt  20057  orngsqr  20783  ornglmulle  20784  orngrmulle  20785  ofldchr  21515  umgr2edg  29189  2pthfrgr  30266  isarchi3  33163  archirngz  33165  archiabllem1a  33167  archiabllem1b  33168  archiabllem2a  33170  archiabllem2c  33171  lineext  36141  brsegle2  36174  cvrcmp  39402  cvrcmp2  39403  atcvreq0  39433  cvlatexch3  39457  cvlcvr1  39458  cvlsupr2  39462  cvlsupr7  39467  atnlej1  39498  atnlej2  39499  cvrval3  39532  ltltncvr  39542  atcvrneN  39549  atcvrj2b  39551  atbtwnex  39567  3noncolr2  39568  3noncolr1N  39569  4noncolr3  39572  3dimlem2  39578  3dimlem3a  39579  3dimlem3  39580  3dimlem3OLDN  39581  3dimlem4a  39582  3dimlem4  39583  3dimlem4OLDN  39584  ps-1  39596  hlatexch4  39600  3atlem1  39602  3atlem2  39603  3atlem3  39604  3atlem4  39605  3atlem5  39606  3atlem6  39607  3atlem7  39608  2llnmat  39643  ps-2c  39647  lplnri3N  39674  lplnexllnN  39683  2llnmeqat  39690  4atlem0a  39712  4atlem0ae  39713  4atlem0be  39714  4atlem9  39722  4atlem10a  39723  4atlem10b  39724  4atlem10  39725  4atlem11a  39726  4atlem11  39728  4atlem12a  39729  dalemcnes  39769  dalempnes  39770  dalemqnet  39771  dalem1  39778  dalemdea  39781  dalem3  39783  dalem5  39786  dalem-cly  39790  dalem27  39818  dalem28  39819  dalem41  39832  dalem45  39836  dalem48  39839  lneq2at  39897  2lnat  39903  2llnma1  39906  2llnma3r  39907  2llnma2  39908  cdlemblem  39912  paddasslem2  39940  pmodl42N  39970  hlmod1i  39975  atmod1i1m  39977  atmod2i1  39980  atmod2i2  39981  atmod3i1  39983  llnexchb2lem  39987  dalawlem2  39991  dalawlem3  39992  dalawlem6  39995  dalawlem7  39996  dalawlem11  40000  dalawlem12  40001  pexmidlem3N  40091  lhpexle3lem  40130  lhpmcvr3  40144  lhp2at0  40151  lhpelim  40156  lhpmod2i2  40157  lhpmod6i1  40158  4atexlempns  40181  4atexlemunv  40185  4atexlemc  40188  4atexlemnclw  40189  4atexlemex2  40190  4atexlemex6  40193  4atex  40195  4atex3  40200  trljat1  40285  trljat2  40286  ltrnatlw  40302  trlval4  40307  cdlemc1  40310  cdlemc3  40312  cdlemc6  40315  cdlemd3  40319  cdlemd4  40320  cdlemd5  40321  cdlemd6  40322  cdlemd7  40323  cdleme00a  40328  cdleme0cp  40333  cdleme0cq  40334  cdleme0e  40336  cdleme02N  40341  cdleme0ex2N  40343  cdleme0moN  40344  cdleme1  40346  cdleme2  40347  cdleme3e  40351  cdleme3g  40353  cdleme3h  40354  cdleme4  40357  cdleme5  40359  cdleme7aa  40361  cdleme7c  40364  cdleme7d  40365  cdleme7e  40366  cdleme8  40369  cdleme9  40372  cdleme10  40373  cdleme16aN  40378  cdleme11a  40379  cdleme11c  40380  cdleme11dN  40381  cdleme11e  40382  cdleme11g  40384  cdleme11h  40385  cdleme11j  40386  cdleme11k  40387  cdleme12  40390  cdleme15a  40393  cdleme15b  40394  cdleme16b  40398  cdleme17c  40407  cdleme0nex  40409  cdleme18d  40414  cdlemednpq  40418  cdleme20zN  40420  cdleme20y  40421  cdleme19a  40422  cdleme19d  40425  cdleme20aN  40428  cdleme20c  40430  cdleme20i  40436  cdleme20j  40437  cdleme21a  40444  cdleme21b  40445  cdleme21c  40446  cdleme21ct  40448  cdleme22cN  40461  cdleme22d  40462  cdleme22e  40463  cdleme22eALTN  40464  cdleme22f  40465  cdleme22f2  40466  cdleme22g  40467  cdleme23c  40470  cdleme41sn3a  40552  cdleme32le  40566  cdleme35b  40569  cdleme35c  40570  cdleme35d  40571  cdleme35e  40572  cdleme36a  40579  cdleme37m  40581  cdleme39a  40584  cdleme42a  40590  cdleme17d2  40614  cdlemeg46frv  40644  cdlemeg46rgv  40647  cdlemf1  40680  cdlemg2fv2  40719  cdlemg2l  40722  cdlemg2m  40723  cdlemg4d  40732  cdlemg4e  40733  cdlemg4f  40734  cdlemg4  40736  cdlemg6c  40739  cdlemg9a  40751  cdlemg10bALTN  40755  cdlemg12a  40762  cdlemg13  40771  cdlemg14f  40772  cdlemg14g  40773  cdlemg17i  40788  cdlemg17pq  40791  cdlemg19  40803  cdlemg21  40805  cdlemg27b  40815  cdlemg33c  40827  cdlemg33d  40828  trlcoabs2N  40841  cdlemg43  40849  cdlemg44b  40851  cdlemg44  40852  cdlemh1  40934  cdlemh2  40935  cdlemi1  40937  tendo0mul  40945  tendo0mulr  40946  cdlemk4  40953  cdlemk9  40958  cdlemk9bN  40959  cdlemk14  40973  cdlemkfid1N  41040  cdlemkid1  41041  cdlemk35s-id  41057  cdlemk39s-id  41059  cdlemk55a  41078  cdlemk55u  41085  cdlemk39u  41087  cdlemk19u  41089  cdlemk56  41090  cdleml8  41102  dia2dimlem1  41183  dia2dimlem2  41184  dia2dimlem3  41185  cdlemn10  41325  dihjust  41336  dihord1  41337  dihlsscpre  41353  dihvalcqpre  41354  dihglbcpreN  41419  dihmeetlem5  41427  dihmeetlem7N  41429  dihjatc1  41430  modmknepk  47486  modm2nep1  47490  modp2nep1  47491  modm1nep2  47492  modm1nem2  47493  lincreslvec3  48607  isldepslvec2  48610