Theorem syl131anc 1410

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401  df-3an 1105

This theorem is used by:  syl132anc  1415  syl231anc  1417  syl133anc  1420  initoeu2lem1  18075  estrres  18199  mulgdir  19176  omndadd2d  20204  omndadd2rd  20205  submomnd  20206  omndmul2  20207  omndmul3  20208  ogrpinv0le  20210  ogrpsub  20211  ogrpaddltbi  20213  ogrpaddltrd  20214  ogrpinv0lt  20217  orngsqr  20978  ornglmulle  20979  orngrmulle  20980  ofldchr  21735  umgr2edg  29568  2pthfrgr  30644  isarchi3  33516  archirngz  33518  archiabllem1a  33520  archiabllem1b  33521  archiabllem2a  33523  archiabllem2c  33524  lineext  36576  brsegle2  36609  cvrcmp  40085  cvrcmp2  40086  atcvreq0  40116  cvlatexch3  40140  cvlcvr1  40141  cvlsupr2  40145  cvlsupr7  40150  atnlej1  40181  atnlej2  40182  cvrval3  40215  ltltncvr  40225  atcvrneN  40232  atcvrj2b  40234  atbtwnex  40250  3noncolr2  40251  3noncolr1N  40252  4noncolr3  40255  3dimlem2  40261  3dimlem3a  40262  3dimlem3  40263  3dimlem3OLDN  40264  3dimlem4a  40265  3dimlem4  40266  3dimlem4OLDN  40267  ps-1  40279  hlatexch4  40283  3atlem1  40285  3atlem2  40286  3atlem3  40287  3atlem4  40288  3atlem5  40289  3atlem6  40290  3atlem7  40291  2llnmat  40326  ps-2c  40330  lplnri3N  40357  lplnexllnN  40366  2llnmeqat  40373  4atlem0a  40395  4atlem0ae  40396  4atlem0be  40397  4atlem9  40405  4atlem10a  40406  4atlem10b  40407  4atlem10  40408  4atlem11a  40409  4atlem11  40411  4atlem12a  40412  dalemcnes  40452  dalempnes  40453  dalemqnet  40454  dalem1  40461  dalemdea  40464  dalem3  40466  dalem5  40469  dalem-cly  40473  dalem27  40501  dalem28  40502  dalem41  40515  dalem45  40519  dalem48  40522  lneq2at  40580  2lnat  40586  2llnma1  40589  2llnma3r  40590  2llnma2  40591  cdlemblem  40595  paddasslem2  40623  pmodl42N  40653  hlmod1i  40658  atmod1i1m  40660  atmod2i1  40663  atmod2i2  40664  atmod3i1  40666  llnexchb2lem  40670  dalawlem2  40674  dalawlem3  40675  dalawlem6  40678  dalawlem7  40679  dalawlem11  40683  dalawlem12  40684  pexmidlem3N  40774  lhpexle3lem  40813  lhpmcvr3  40827  lhp2at0  40834  lhpelim  40839  lhpmod2i2  40840  lhpmod6i1  40841  4atexlempns  40864  4atexlemunv  40868  4atexlemc  40871  4atexlemnclw  40872  4atexlemex2  40873  4atexlemex6  40876  4atex  40878  4atex3  40883  trljat1  40968  trljat2  40969  ltrnatlw  40985  trlval4  40990  cdlemc1  40993  cdlemc3  40995  cdlemc6  40998  cdlemd3  41002  cdlemd4  41003  cdlemd5  41004  cdlemd6  41005  cdlemd7  41006  cdleme00a  41011  cdleme0cp  41016  cdleme0cq  41017  cdleme0e  41019  cdleme02N  41024  cdleme0ex2N  41026  cdleme0moN  41027  cdleme1  41029  cdleme2  41030  cdleme3e  41034  cdleme3g  41036  cdleme3h  41037  cdleme4  41040  cdleme5  41042  cdleme7aa  41044  cdleme7c  41047  cdleme7d  41048  cdleme7e  41049  cdleme8  41052  cdleme9  41055  cdleme10  41056  cdleme16aN  41061  cdleme11a  41062  cdleme11c  41063  cdleme11dN  41064  cdleme11e  41065  cdleme11g  41067  cdleme11h  41068  cdleme11j  41069  cdleme11k  41070  cdleme12  41073  cdleme15a  41076  cdleme15b  41077  cdleme16b  41081  cdleme17c  41090  cdleme0nex  41092  cdleme18d  41097  cdlemednpq  41101  cdleme20zN  41103  cdleme20y  41104  cdleme19a  41105  cdleme19d  41108  cdleme20aN  41111  cdleme20c  41113  cdleme20i  41119  cdleme20j  41120  cdleme21a  41127  cdleme21b  41128  cdleme21c  41129  cdleme21ct  41131  cdleme22cN  41144  cdleme22d  41145  cdleme22e  41146  cdleme22eALTN  41147  cdleme22f  41148  cdleme22f2  41149  cdleme22g  41150  cdleme23c  41153  cdleme41sn3a  41235  cdleme32le  41249  cdleme35b  41252  cdleme35c  41253  cdleme35d  41254  cdleme35e  41255  cdleme36a  41262  cdleme37m  41264  cdleme39a  41267  cdleme42a  41273  cdleme17d2  41297  cdlemeg46frv  41327  cdlemeg46rgv  41330  cdlemf1  41363  cdlemg2fv2  41402  cdlemg2l  41405  cdlemg2m  41406  cdlemg4d  41415  cdlemg4e  41416  cdlemg4f  41417  cdlemg4  41419  cdlemg6c  41422  cdlemg9a  41434  cdlemg10bALTN  41438  cdlemg12a  41445  cdlemg13  41454  cdlemg14f  41455  cdlemg14g  41456  cdlemg17i  41471  cdlemg17pq  41474  cdlemg19  41486  cdlemg21  41488  cdlemg27b  41498  cdlemg33c  41510  cdlemg33d  41511  trlcoabs2N  41524  cdlemg43  41532  cdlemg44b  41534  cdlemg44  41535  cdlemh1  41617  cdlemh2  41618  cdlemi1  41620  tendo0mul  41628  tendo0mulr  41629  cdlemk4  41636  cdlemk9  41641  cdlemk9bN  41642  cdlemk14  41656  cdlemkfid1N  41723  cdlemkid1  41724  cdlemk35s-id  41740  cdlemk39s-id  41742  cdlemk55a  41761  cdlemk55u  41768  cdlemk39u  41770  cdlemk19u  41772  cdlemk56  41773  cdleml8  41785  dia2dimlem1  41866  dia2dimlem2  41867  dia2dimlem3  41868  cdlemn10  42008  dihjust  42019  dihord1  42020  dihlsscpre  42036  dihvalcqpre  42037  dihglbcpreN  42102  dihmeetlem5  42110  dihmeetlem7N  42112  dihjatc1  42113  modmknepk  48133  modm2nep1  48137  modp2nep1  48138  modm1nep2  48139  modm1nem2  48140  lincreslvec3  49290  isldepslvec2  49293