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 1129	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃 ∧ 𝜏))
6		syl23anc.5	. 2 ⊢ (𝜑 → 𝜂)
7		syl131anc.6	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁)
8	1, 5, 6, 7	syl3anc 1373	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  1390  syl231anc  1392  syl133anc  1395  initoeu2lem1  18059  estrres  18184  mulgdir  19124  umgr2edg  29226  2pthfrgr  30303  omndadd2d  33085  omndadd2rd  33086  submomnd  33087  omndmul2  33089  omndmul3  33090  ogrpinv0le  33092  ogrpsub  33093  ogrpaddltbi  33095  ogrpaddltrd  33096  ogrpinv0lt  33099  isarchi3  33194  archirngz  33196  archiabllem1a  33198  archiabllem1b  33199  archiabllem2a  33201  archiabllem2c  33202  orngsqr  33334  ornglmulle  33335  orngrmulle  33336  ofldchr  33344  lineext  36077  brsegle2  36110  cvrcmp  39284  cvrcmp2  39285  atcvreq0  39315  cvlatexch3  39339  cvlcvr1  39340  cvlsupr2  39344  cvlsupr7  39349  atnlej1  39381  atnlej2  39382  cvrval3  39415  ltltncvr  39425  atcvrneN  39432  atcvrj2b  39434  atbtwnex  39450  3noncolr2  39451  3noncolr1N  39452  4noncolr3  39455  3dimlem2  39461  3dimlem3a  39462  3dimlem3  39463  3dimlem3OLDN  39464  3dimlem4a  39465  3dimlem4  39466  3dimlem4OLDN  39467  ps-1  39479  hlatexch4  39483  3atlem1  39485  3atlem2  39486  3atlem3  39487  3atlem4  39488  3atlem5  39489  3atlem6  39490  3atlem7  39491  2llnmat  39526  ps-2c  39530  lplnri3N  39557  lplnexllnN  39566  2llnmeqat  39573  4atlem0a  39595  4atlem0ae  39596  4atlem0be  39597  4atlem9  39605  4atlem10a  39606  4atlem10b  39607  4atlem10  39608  4atlem11a  39609  4atlem11  39611  4atlem12a  39612  dalemcnes  39652  dalempnes  39653  dalemqnet  39654  dalem1  39661  dalemdea  39664  dalem3  39666  dalem5  39669  dalem-cly  39673  dalem27  39701  dalem28  39702  dalem41  39715  dalem45  39719  dalem48  39722  lneq2at  39780  2lnat  39786  2llnma1  39789  2llnma3r  39790  2llnma2  39791  cdlemblem  39795  paddasslem2  39823  pmodl42N  39853  hlmod1i  39858  atmod1i1m  39860  atmod2i1  39863  atmod2i2  39864  atmod3i1  39866  llnexchb2lem  39870  dalawlem2  39874  dalawlem3  39875  dalawlem6  39878  dalawlem7  39879  dalawlem11  39883  dalawlem12  39884  pexmidlem3N  39974  lhpexle3lem  40013  lhpmcvr3  40027  lhp2at0  40034  lhpelim  40039  lhpmod2i2  40040  lhpmod6i1  40041  4atexlempns  40064  4atexlemunv  40068  4atexlemc  40071  4atexlemnclw  40072  4atexlemex2  40073  4atexlemex6  40076  4atex  40078  4atex3  40083  trljat1  40168  trljat2  40169  ltrnatlw  40185  trlval4  40190  cdlemc1  40193  cdlemc3  40195  cdlemc6  40198  cdlemd3  40202  cdlemd4  40203  cdlemd5  40204  cdlemd6  40205  cdlemd7  40206  cdleme00a  40211  cdleme0cp  40216  cdleme0cq  40217  cdleme0e  40219  cdleme02N  40224  cdleme0ex2N  40226  cdleme0moN  40227  cdleme1  40229  cdleme2  40230  cdleme3e  40234  cdleme3g  40236  cdleme3h  40237  cdleme4  40240  cdleme5  40242  cdleme7aa  40244  cdleme7c  40247  cdleme7d  40248  cdleme7e  40249  cdleme8  40252  cdleme9  40255  cdleme10  40256  cdleme16aN  40261  cdleme11a  40262  cdleme11c  40263  cdleme11dN  40264  cdleme11e  40265  cdleme11g  40267  cdleme11h  40268  cdleme11j  40269  cdleme11k  40270  cdleme12  40273  cdleme15a  40276  cdleme15b  40277  cdleme16b  40281  cdleme17c  40290  cdleme0nex  40292  cdleme18d  40297  cdlemednpq  40301  cdleme20zN  40303  cdleme20y  40304  cdleme19a  40305  cdleme19d  40308  cdleme20aN  40311  cdleme20c  40313  cdleme20i  40319  cdleme20j  40320  cdleme21a  40327  cdleme21b  40328  cdleme21c  40329  cdleme21ct  40331  cdleme22cN  40344  cdleme22d  40345  cdleme22e  40346  cdleme22eALTN  40347  cdleme22f  40348  cdleme22f2  40349  cdleme22g  40350  cdleme23c  40353  cdleme41sn3a  40435  cdleme32le  40449  cdleme35b  40452  cdleme35c  40453  cdleme35d  40454  cdleme35e  40455  cdleme36a  40462  cdleme37m  40464  cdleme39a  40467  cdleme42a  40473  cdleme17d2  40497  cdlemeg46frv  40527  cdlemeg46rgv  40530  cdlemf1  40563  cdlemg2fv2  40602  cdlemg2l  40605  cdlemg2m  40606  cdlemg4d  40615  cdlemg4e  40616  cdlemg4f  40617  cdlemg4  40619  cdlemg6c  40622  cdlemg9a  40634  cdlemg10bALTN  40638  cdlemg12a  40645  cdlemg13  40654  cdlemg14f  40655  cdlemg14g  40656  cdlemg17i  40671  cdlemg17pq  40674  cdlemg19  40686  cdlemg21  40688  cdlemg27b  40698  cdlemg33c  40710  cdlemg33d  40711  trlcoabs2N  40724  cdlemg43  40732  cdlemg44b  40734  cdlemg44  40735  cdlemh1  40817  cdlemh2  40818  cdlemi1  40820  tendo0mul  40828  tendo0mulr  40829  cdlemk4  40836  cdlemk9  40841  cdlemk9bN  40842  cdlemk14  40856  cdlemkfid1N  40923  cdlemkid1  40924  cdlemk35s-id  40940  cdlemk39s-id  40942  cdlemk55a  40961  cdlemk55u  40968  cdlemk39u  40970  cdlemk19u  40972  cdlemk56  40973  cdleml8  40985  dia2dimlem1  41066  dia2dimlem2  41067  dia2dimlem3  41068  cdlemn10  41208  dihjust  41219  dihord1  41220  dihlsscpre  41236  dihvalcqpre  41237  dihglbcpreN  41302  dihmeetlem5  41310  dihmeetlem7N  41312  dihjatc1  41313  gpg3nbgrvtxlem  48023  lincreslvec3  48399  isldepslvec2  48402