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  17976  estrres  18100  mulgdir  19038  umgr2edg  29136  2pthfrgr  30213  omndadd2d  33022  omndadd2rd  33023  submomnd  33024  omndmul2  33026  omndmul3  33027  ogrpinv0le  33029  ogrpsub  33030  ogrpaddltbi  33032  ogrpaddltrd  33033  ogrpinv0lt  33036  isarchi3  33141  archirngz  33143  archiabllem1a  33145  archiabllem1b  33146  archiabllem2a  33148  archiabllem2c  33149  orngsqr  33282  ornglmulle  33283  orngrmulle  33284  ofldchr  33292  lineext  36064  brsegle2  36097  cvrcmp  39276  cvrcmp2  39277  atcvreq0  39307  cvlatexch3  39331  cvlcvr1  39332  cvlsupr2  39336  cvlsupr7  39341  atnlej1  39373  atnlej2  39374  cvrval3  39407  ltltncvr  39417  atcvrneN  39424  atcvrj2b  39426  atbtwnex  39442  3noncolr2  39443  3noncolr1N  39444  4noncolr3  39447  3dimlem2  39453  3dimlem3a  39454  3dimlem3  39455  3dimlem3OLDN  39456  3dimlem4a  39457  3dimlem4  39458  3dimlem4OLDN  39459  ps-1  39471  hlatexch4  39475  3atlem1  39477  3atlem2  39478  3atlem3  39479  3atlem4  39480  3atlem5  39481  3atlem6  39482  3atlem7  39483  2llnmat  39518  ps-2c  39522  lplnri3N  39549  lplnexllnN  39558  2llnmeqat  39565  4atlem0a  39587  4atlem0ae  39588  4atlem0be  39589  4atlem9  39597  4atlem10a  39598  4atlem10b  39599  4atlem10  39600  4atlem11a  39601  4atlem11  39603  4atlem12a  39604  dalemcnes  39644  dalempnes  39645  dalemqnet  39646  dalem1  39653  dalemdea  39656  dalem3  39658  dalem5  39661  dalem-cly  39665  dalem27  39693  dalem28  39694  dalem41  39707  dalem45  39711  dalem48  39714  lneq2at  39772  2lnat  39778  2llnma1  39781  2llnma3r  39782  2llnma2  39783  cdlemblem  39787  paddasslem2  39815  pmodl42N  39845  hlmod1i  39850  atmod1i1m  39852  atmod2i1  39855  atmod2i2  39856  atmod3i1  39858  llnexchb2lem  39862  dalawlem2  39866  dalawlem3  39867  dalawlem6  39870  dalawlem7  39871  dalawlem11  39875  dalawlem12  39876  pexmidlem3N  39966  lhpexle3lem  40005  lhpmcvr3  40019  lhp2at0  40026  lhpelim  40031  lhpmod2i2  40032  lhpmod6i1  40033  4atexlempns  40056  4atexlemunv  40060  4atexlemc  40063  4atexlemnclw  40064  4atexlemex2  40065  4atexlemex6  40068  4atex  40070  4atex3  40075  trljat1  40160  trljat2  40161  ltrnatlw  40177  trlval4  40182  cdlemc1  40185  cdlemc3  40187  cdlemc6  40190  cdlemd3  40194  cdlemd4  40195  cdlemd5  40196  cdlemd6  40197  cdlemd7  40198  cdleme00a  40203  cdleme0cp  40208  cdleme0cq  40209  cdleme0e  40211  cdleme02N  40216  cdleme0ex2N  40218  cdleme0moN  40219  cdleme1  40221  cdleme2  40222  cdleme3e  40226  cdleme3g  40228  cdleme3h  40229  cdleme4  40232  cdleme5  40234  cdleme7aa  40236  cdleme7c  40239  cdleme7d  40240  cdleme7e  40241  cdleme8  40244  cdleme9  40247  cdleme10  40248  cdleme16aN  40253  cdleme11a  40254  cdleme11c  40255  cdleme11dN  40256  cdleme11e  40257  cdleme11g  40259  cdleme11h  40260  cdleme11j  40261  cdleme11k  40262  cdleme12  40265  cdleme15a  40268  cdleme15b  40269  cdleme16b  40273  cdleme17c  40282  cdleme0nex  40284  cdleme18d  40289  cdlemednpq  40293  cdleme20zN  40295  cdleme20y  40296  cdleme19a  40297  cdleme19d  40300  cdleme20aN  40303  cdleme20c  40305  cdleme20i  40311  cdleme20j  40312  cdleme21a  40319  cdleme21b  40320  cdleme21c  40321  cdleme21ct  40323  cdleme22cN  40336  cdleme22d  40337  cdleme22e  40338  cdleme22eALTN  40339  cdleme22f  40340  cdleme22f2  40341  cdleme22g  40342  cdleme23c  40345  cdleme41sn3a  40427  cdleme32le  40441  cdleme35b  40444  cdleme35c  40445  cdleme35d  40446  cdleme35e  40447  cdleme36a  40454  cdleme37m  40456  cdleme39a  40459  cdleme42a  40465  cdleme17d2  40489  cdlemeg46frv  40519  cdlemeg46rgv  40522  cdlemf1  40555  cdlemg2fv2  40594  cdlemg2l  40597  cdlemg2m  40598  cdlemg4d  40607  cdlemg4e  40608  cdlemg4f  40609  cdlemg4  40611  cdlemg6c  40614  cdlemg9a  40626  cdlemg10bALTN  40630  cdlemg12a  40637  cdlemg13  40646  cdlemg14f  40647  cdlemg14g  40648  cdlemg17i  40663  cdlemg17pq  40666  cdlemg19  40678  cdlemg21  40680  cdlemg27b  40690  cdlemg33c  40702  cdlemg33d  40703  trlcoabs2N  40716  cdlemg43  40724  cdlemg44b  40726  cdlemg44  40727  cdlemh1  40809  cdlemh2  40810  cdlemi1  40812  tendo0mul  40820  tendo0mulr  40821  cdlemk4  40828  cdlemk9  40833  cdlemk9bN  40834  cdlemk14  40848  cdlemkfid1N  40915  cdlemkid1  40916  cdlemk35s-id  40932  cdlemk39s-id  40934  cdlemk55a  40953  cdlemk55u  40960  cdlemk39u  40962  cdlemk19u  40964  cdlemk56  40965  cdleml8  40977  dia2dimlem1  41058  dia2dimlem2  41059  dia2dimlem3  41060  cdlemn10  41200  dihjust  41211  dihord1  41212  dihlsscpre  41228  dihvalcqpre  41229  dihglbcpreN  41294  dihmeetlem5  41302  dihmeetlem7N  41304  dihjatc1  41305  modmknepk  47363  modm2nep1  47367  modp2nep1  47368  modm1nep2  47369  modm1nem2  47370  lincreslvec3  48471  isldepslvec2  48474