Theorem syl131anc 1386

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  syl132anc  1391  syl231anc  1393  syl133anc  1396  initoeu2lem1  17972  estrres  18096  mulgdir  19073  omndadd2d  20096  omndadd2rd  20097  submomnd  20098  omndmul2  20099  omndmul3  20100  ogrpinv0le  20102  ogrpsub  20103  ogrpaddltbi  20105  ogrpaddltrd  20106  ogrpinv0lt  20109  orngsqr  20834  ornglmulle  20835  orngrmulle  20836  ofldchr  21566  umgr2edg  29292  2pthfrgr  30369  isarchi3  33263  archirngz  33265  archiabllem1a  33267  archiabllem1b  33268  archiabllem2a  33270  archiabllem2c  33271  lineext  36274  brsegle2  36307  cvrcmp  39743  cvrcmp2  39744  atcvreq0  39774  cvlatexch3  39798  cvlcvr1  39799  cvlsupr2  39803  cvlsupr7  39808  atnlej1  39839  atnlej2  39840  cvrval3  39873  ltltncvr  39883  atcvrneN  39890  atcvrj2b  39892  atbtwnex  39908  3noncolr2  39909  3noncolr1N  39910  4noncolr3  39913  3dimlem2  39919  3dimlem3a  39920  3dimlem3  39921  3dimlem3OLDN  39922  3dimlem4a  39923  3dimlem4  39924  3dimlem4OLDN  39925  ps-1  39937  hlatexch4  39941  3atlem1  39943  3atlem2  39944  3atlem3  39945  3atlem4  39946  3atlem5  39947  3atlem6  39948  3atlem7  39949  2llnmat  39984  ps-2c  39988  lplnri3N  40015  lplnexllnN  40024  2llnmeqat  40031  4atlem0a  40053  4atlem0ae  40054  4atlem0be  40055  4atlem9  40063  4atlem10a  40064  4atlem10b  40065  4atlem10  40066  4atlem11a  40067  4atlem11  40069  4atlem12a  40070  dalemcnes  40110  dalempnes  40111  dalemqnet  40112  dalem1  40119  dalemdea  40122  dalem3  40124  dalem5  40127  dalem-cly  40131  dalem27  40159  dalem28  40160  dalem41  40173  dalem45  40177  dalem48  40180  lneq2at  40238  2lnat  40244  2llnma1  40247  2llnma3r  40248  2llnma2  40249  cdlemblem  40253  paddasslem2  40281  pmodl42N  40311  hlmod1i  40316  atmod1i1m  40318  atmod2i1  40321  atmod2i2  40322  atmod3i1  40324  llnexchb2lem  40328  dalawlem2  40332  dalawlem3  40333  dalawlem6  40336  dalawlem7  40337  dalawlem11  40341  dalawlem12  40342  pexmidlem3N  40432  lhpexle3lem  40471  lhpmcvr3  40485  lhp2at0  40492  lhpelim  40497  lhpmod2i2  40498  lhpmod6i1  40499  4atexlempns  40522  4atexlemunv  40526  4atexlemc  40529  4atexlemnclw  40530  4atexlemex2  40531  4atexlemex6  40534  4atex  40536  4atex3  40541  trljat1  40626  trljat2  40627  ltrnatlw  40643  trlval4  40648  cdlemc1  40651  cdlemc3  40653  cdlemc6  40656  cdlemd3  40660  cdlemd4  40661  cdlemd5  40662  cdlemd6  40663  cdlemd7  40664  cdleme00a  40669  cdleme0cp  40674  cdleme0cq  40675  cdleme0e  40677  cdleme02N  40682  cdleme0ex2N  40684  cdleme0moN  40685  cdleme1  40687  cdleme2  40688  cdleme3e  40692  cdleme3g  40694  cdleme3h  40695  cdleme4  40698  cdleme5  40700  cdleme7aa  40702  cdleme7c  40705  cdleme7d  40706  cdleme7e  40707  cdleme8  40710  cdleme9  40713  cdleme10  40714  cdleme16aN  40719  cdleme11a  40720  cdleme11c  40721  cdleme11dN  40722  cdleme11e  40723  cdleme11g  40725  cdleme11h  40726  cdleme11j  40727  cdleme11k  40728  cdleme12  40731  cdleme15a  40734  cdleme15b  40735  cdleme16b  40739  cdleme17c  40748  cdleme0nex  40750  cdleme18d  40755  cdlemednpq  40759  cdleme20zN  40761  cdleme20y  40762  cdleme19a  40763  cdleme19d  40766  cdleme20aN  40769  cdleme20c  40771  cdleme20i  40777  cdleme20j  40778  cdleme21a  40785  cdleme21b  40786  cdleme21c  40787  cdleme21ct  40789  cdleme22cN  40802  cdleme22d  40803  cdleme22e  40804  cdleme22eALTN  40805  cdleme22f  40806  cdleme22f2  40807  cdleme22g  40808  cdleme23c  40811  cdleme41sn3a  40893  cdleme32le  40907  cdleme35b  40910  cdleme35c  40911  cdleme35d  40912  cdleme35e  40913  cdleme36a  40920  cdleme37m  40922  cdleme39a  40925  cdleme42a  40931  cdleme17d2  40955  cdlemeg46frv  40985  cdlemeg46rgv  40988  cdlemf1  41021  cdlemg2fv2  41060  cdlemg2l  41063  cdlemg2m  41064  cdlemg4d  41073  cdlemg4e  41074  cdlemg4f  41075  cdlemg4  41077  cdlemg6c  41080  cdlemg9a  41092  cdlemg10bALTN  41096  cdlemg12a  41103  cdlemg13  41112  cdlemg14f  41113  cdlemg14g  41114  cdlemg17i  41129  cdlemg17pq  41132  cdlemg19  41144  cdlemg21  41146  cdlemg27b  41156  cdlemg33c  41168  cdlemg33d  41169  trlcoabs2N  41182  cdlemg43  41190  cdlemg44b  41192  cdlemg44  41193  cdlemh1  41275  cdlemh2  41276  cdlemi1  41278  tendo0mul  41286  tendo0mulr  41287  cdlemk4  41294  cdlemk9  41299  cdlemk9bN  41300  cdlemk14  41314  cdlemkfid1N  41381  cdlemkid1  41382  cdlemk35s-id  41398  cdlemk39s-id  41400  cdlemk55a  41419  cdlemk55u  41426  cdlemk39u  41428  cdlemk19u  41430  cdlemk56  41431  cdleml8  41443  dia2dimlem1  41524  dia2dimlem2  41525  dia2dimlem3  41526  cdlemn10  41666  dihjust  41677  dihord1  41678  dihlsscpre  41694  dihvalcqpre  41695  dihglbcpreN  41760  dihmeetlem5  41768  dihmeetlem7N  41770  dihjatc1  41771  modmknepk  47828  modm2nep1  47832  modp2nep1  47833  modm1nep2  47834  modm1nem2  47835  lincreslvec3  48970  isldepslvec2  48973