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  17983  estrres  18107  mulgdir  19045  umgr2edg  29143  2pthfrgr  30220  omndadd2d  33029  omndadd2rd  33030  submomnd  33031  omndmul2  33033  omndmul3  33034  ogrpinv0le  33036  ogrpsub  33037  ogrpaddltbi  33039  ogrpaddltrd  33040  ogrpinv0lt  33043  isarchi3  33148  archirngz  33150  archiabllem1a  33152  archiabllem1b  33153  archiabllem2a  33155  archiabllem2c  33156  orngsqr  33289  ornglmulle  33290  orngrmulle  33291  ofldchr  33299  lineext  36071  brsegle2  36104  cvrcmp  39283  cvrcmp2  39284  atcvreq0  39314  cvlatexch3  39338  cvlcvr1  39339  cvlsupr2  39343  cvlsupr7  39348  atnlej1  39380  atnlej2  39381  cvrval3  39414  ltltncvr  39424  atcvrneN  39431  atcvrj2b  39433  atbtwnex  39449  3noncolr2  39450  3noncolr1N  39451  4noncolr3  39454  3dimlem2  39460  3dimlem3a  39461  3dimlem3  39462  3dimlem3OLDN  39463  3dimlem4a  39464  3dimlem4  39465  3dimlem4OLDN  39466  ps-1  39478  hlatexch4  39482  3atlem1  39484  3atlem2  39485  3atlem3  39486  3atlem4  39487  3atlem5  39488  3atlem6  39489  3atlem7  39490  2llnmat  39525  ps-2c  39529  lplnri3N  39556  lplnexllnN  39565  2llnmeqat  39572  4atlem0a  39594  4atlem0ae  39595  4atlem0be  39596  4atlem9  39604  4atlem10a  39605  4atlem10b  39606  4atlem10  39607  4atlem11a  39608  4atlem11  39610  4atlem12a  39611  dalemcnes  39651  dalempnes  39652  dalemqnet  39653  dalem1  39660  dalemdea  39663  dalem3  39665  dalem5  39668  dalem-cly  39672  dalem27  39700  dalem28  39701  dalem41  39714  dalem45  39718  dalem48  39721  lneq2at  39779  2lnat  39785  2llnma1  39788  2llnma3r  39789  2llnma2  39790  cdlemblem  39794  paddasslem2  39822  pmodl42N  39852  hlmod1i  39857  atmod1i1m  39859  atmod2i1  39862  atmod2i2  39863  atmod3i1  39865  llnexchb2lem  39869  dalawlem2  39873  dalawlem3  39874  dalawlem6  39877  dalawlem7  39878  dalawlem11  39882  dalawlem12  39883  pexmidlem3N  39973  lhpexle3lem  40012  lhpmcvr3  40026  lhp2at0  40033  lhpelim  40038  lhpmod2i2  40039  lhpmod6i1  40040  4atexlempns  40063  4atexlemunv  40067  4atexlemc  40070  4atexlemnclw  40071  4atexlemex2  40072  4atexlemex6  40075  4atex  40077  4atex3  40082  trljat1  40167  trljat2  40168  ltrnatlw  40184  trlval4  40189  cdlemc1  40192  cdlemc3  40194  cdlemc6  40197  cdlemd3  40201  cdlemd4  40202  cdlemd5  40203  cdlemd6  40204  cdlemd7  40205  cdleme00a  40210  cdleme0cp  40215  cdleme0cq  40216  cdleme0e  40218  cdleme02N  40223  cdleme0ex2N  40225  cdleme0moN  40226  cdleme1  40228  cdleme2  40229  cdleme3e  40233  cdleme3g  40235  cdleme3h  40236  cdleme4  40239  cdleme5  40241  cdleme7aa  40243  cdleme7c  40246  cdleme7d  40247  cdleme7e  40248  cdleme8  40251  cdleme9  40254  cdleme10  40255  cdleme16aN  40260  cdleme11a  40261  cdleme11c  40262  cdleme11dN  40263  cdleme11e  40264  cdleme11g  40266  cdleme11h  40267  cdleme11j  40268  cdleme11k  40269  cdleme12  40272  cdleme15a  40275  cdleme15b  40276  cdleme16b  40280  cdleme17c  40289  cdleme0nex  40291  cdleme18d  40296  cdlemednpq  40300  cdleme20zN  40302  cdleme20y  40303  cdleme19a  40304  cdleme19d  40307  cdleme20aN  40310  cdleme20c  40312  cdleme20i  40318  cdleme20j  40319  cdleme21a  40326  cdleme21b  40327  cdleme21c  40328  cdleme21ct  40330  cdleme22cN  40343  cdleme22d  40344  cdleme22e  40345  cdleme22eALTN  40346  cdleme22f  40347  cdleme22f2  40348  cdleme22g  40349  cdleme23c  40352  cdleme41sn3a  40434  cdleme32le  40448  cdleme35b  40451  cdleme35c  40452  cdleme35d  40453  cdleme35e  40454  cdleme36a  40461  cdleme37m  40463  cdleme39a  40466  cdleme42a  40472  cdleme17d2  40496  cdlemeg46frv  40526  cdlemeg46rgv  40529  cdlemf1  40562  cdlemg2fv2  40601  cdlemg2l  40604  cdlemg2m  40605  cdlemg4d  40614  cdlemg4e  40615  cdlemg4f  40616  cdlemg4  40618  cdlemg6c  40621  cdlemg9a  40633  cdlemg10bALTN  40637  cdlemg12a  40644  cdlemg13  40653  cdlemg14f  40654  cdlemg14g  40655  cdlemg17i  40670  cdlemg17pq  40673  cdlemg19  40685  cdlemg21  40687  cdlemg27b  40697  cdlemg33c  40709  cdlemg33d  40710  trlcoabs2N  40723  cdlemg43  40731  cdlemg44b  40733  cdlemg44  40734  cdlemh1  40816  cdlemh2  40817  cdlemi1  40819  tendo0mul  40827  tendo0mulr  40828  cdlemk4  40835  cdlemk9  40840  cdlemk9bN  40841  cdlemk14  40855  cdlemkfid1N  40922  cdlemkid1  40923  cdlemk35s-id  40939  cdlemk39s-id  40941  cdlemk55a  40960  cdlemk55u  40967  cdlemk39u  40969  cdlemk19u  40971  cdlemk56  40972  cdleml8  40984  dia2dimlem1  41065  dia2dimlem2  41066  dia2dimlem3  41067  cdlemn10  41207  dihjust  41218  dihord1  41219  dihlsscpre  41235  dihvalcqpre  41236  dihglbcpreN  41301  dihmeetlem5  41309  dihmeetlem7N  41311  dihjatc1  41312  modmknepk  47367  modm2nep1  47371  modp2nep1  47372  modm1nep2  47373  modm1nem2  47374  lincreslvec3  48475  isldepslvec2  48478