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 ⊢ (𝜑 → 𝜁)

Syntax hints:   → wi 4   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  syl132anc  1415  syl231anc  1417  syl133anc  1420  initoeu2lem1  18072  estrres  18196  mulgdir  19173  omndadd2d  20201  omndadd2rd  20202  submomnd  20203  omndmul2  20204  omndmul3  20205  ogrpinv0le  20207  ogrpsub  20208  ogrpaddltbi  20210  ogrpaddltrd  20211  ogrpinv0lt  20214  orngsqr  20950  ornglmulle  20951  orngrmulle  20952  ofldchr  21707  umgr2edg  29537  2pthfrgr  30613  isarchi3  33485  archirngz  33487  archiabllem1a  33489  archiabllem1b  33490  archiabllem2a  33492  archiabllem2c  33493  lineext  36546  brsegle2  36579  cvrcmp  40035  cvrcmp2  40036  atcvreq0  40066  cvlatexch3  40090  cvlcvr1  40091  cvlsupr2  40095  cvlsupr7  40100  atnlej1  40131  atnlej2  40132  cvrval3  40165  ltltncvr  40175  atcvrneN  40182  atcvrj2b  40184  atbtwnex  40200  3noncolr2  40201  3noncolr1N  40202  4noncolr3  40205  3dimlem2  40211  3dimlem3a  40212  3dimlem3  40213  3dimlem3OLDN  40214  3dimlem4a  40215  3dimlem4  40216  3dimlem4OLDN  40217  ps-1  40229  hlatexch4  40233  3atlem1  40235  3atlem2  40236  3atlem3  40237  3atlem4  40238  3atlem5  40239  3atlem6  40240  3atlem7  40241  2llnmat  40276  ps-2c  40280  lplnri3N  40307  lplnexllnN  40316  2llnmeqat  40323  4atlem0a  40345  4atlem0ae  40346  4atlem0be  40347  4atlem9  40355  4atlem10a  40356  4atlem10b  40357  4atlem10  40358  4atlem11a  40359  4atlem11  40361  4atlem12a  40362  dalemcnes  40402  dalempnes  40403  dalemqnet  40404  dalem1  40411  dalemdea  40414  dalem3  40416  dalem5  40419  dalem-cly  40423  dalem27  40451  dalem28  40452  dalem41  40465  dalem45  40469  dalem48  40472  lneq2at  40530  2lnat  40536  2llnma1  40539  2llnma3r  40540  2llnma2  40541  cdlemblem  40545  paddasslem2  40573  pmodl42N  40603  hlmod1i  40608  atmod1i1m  40610  atmod2i1  40613  atmod2i2  40614  atmod3i1  40616  llnexchb2lem  40620  dalawlem2  40624  dalawlem3  40625  dalawlem6  40628  dalawlem7  40629  dalawlem11  40633  dalawlem12  40634  pexmidlem3N  40724  lhpexle3lem  40763  lhpmcvr3  40777  lhp2at0  40784  lhpelim  40789  lhpmod2i2  40790  lhpmod6i1  40791  4atexlempns  40814  4atexlemunv  40818  4atexlemc  40821  4atexlemnclw  40822  4atexlemex2  40823  4atexlemex6  40826  4atex  40828  4atex3  40833  trljat1  40918  trljat2  40919  ltrnatlw  40935  trlval4  40940  cdlemc1  40943  cdlemc3  40945  cdlemc6  40948  cdlemd3  40952  cdlemd4  40953  cdlemd5  40954  cdlemd6  40955  cdlemd7  40956  cdleme00a  40961  cdleme0cp  40966  cdleme0cq  40967  cdleme0e  40969  cdleme02N  40974  cdleme0ex2N  40976  cdleme0moN  40977  cdleme1  40979  cdleme2  40980  cdleme3e  40984  cdleme3g  40986  cdleme3h  40987  cdleme4  40990  cdleme5  40992  cdleme7aa  40994  cdleme7c  40997  cdleme7d  40998  cdleme7e  40999  cdleme8  41002  cdleme9  41005  cdleme10  41006  cdleme16aN  41011  cdleme11a  41012  cdleme11c  41013  cdleme11dN  41014  cdleme11e  41015  cdleme11g  41017  cdleme11h  41018  cdleme11j  41019  cdleme11k  41020  cdleme12  41023  cdleme15a  41026  cdleme15b  41027  cdleme16b  41031  cdleme17c  41040  cdleme0nex  41042  cdleme18d  41047  cdlemednpq  41051  cdleme20zN  41053  cdleme20y  41054  cdleme19a  41055  cdleme19d  41058  cdleme20aN  41061  cdleme20c  41063  cdleme20i  41069  cdleme20j  41070  cdleme21a  41077  cdleme21b  41078  cdleme21c  41079  cdleme21ct  41081  cdleme22cN  41094  cdleme22d  41095  cdleme22e  41096  cdleme22eALTN  41097  cdleme22f  41098  cdleme22f2  41099  cdleme22g  41100  cdleme23c  41103  cdleme41sn3a  41185  cdleme32le  41199  cdleme35b  41202  cdleme35c  41203  cdleme35d  41204  cdleme35e  41205  cdleme36a  41212  cdleme37m  41214  cdleme39a  41217  cdleme42a  41223  cdleme17d2  41247  cdlemeg46frv  41277  cdlemeg46rgv  41280  cdlemf1  41313  cdlemg2fv2  41352  cdlemg2l  41355  cdlemg2m  41356  cdlemg4d  41365  cdlemg4e  41366  cdlemg4f  41367  cdlemg4  41369  cdlemg6c  41372  cdlemg9a  41384  cdlemg10bALTN  41388  cdlemg12a  41395  cdlemg13  41404  cdlemg14f  41405  cdlemg14g  41406  cdlemg17i  41421  cdlemg17pq  41424  cdlemg19  41436  cdlemg21  41438  cdlemg27b  41448  cdlemg33c  41460  cdlemg33d  41461  trlcoabs2N  41474  cdlemg43  41482  cdlemg44b  41484  cdlemg44  41485  cdlemh1  41567  cdlemh2  41568  cdlemi1  41570  tendo0mul  41578  tendo0mulr  41579  cdlemk4  41586  cdlemk9  41591  cdlemk9bN  41592  cdlemk14  41606  cdlemkfid1N  41673  cdlemkid1  41674  cdlemk35s-id  41690  cdlemk39s-id  41692  cdlemk55a  41711  cdlemk55u  41718  cdlemk39u  41720  cdlemk19u  41722  cdlemk56  41723  cdleml8  41735  dia2dimlem1  41816  dia2dimlem2  41817  dia2dimlem3  41818  cdlemn10  41958  dihjust  41969  dihord1  41970  dihlsscpre  41986  dihvalcqpre  41987  dihglbcpreN  42052  dihmeetlem5  42060  dihmeetlem7N  42062  dihjatc1  42063  modmknepk  48082  modm2nep1  48086  modp2nep1  48087  modm1nep2  48088  modm1nem2  48089  lincreslvec3  49239  isldepslvec2  49242