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  17938  estrres  18062  mulgdir  19036  omndadd2d  20059  omndadd2rd  20060  submomnd  20061  omndmul2  20062  omndmul3  20063  ogrpinv0le  20065  ogrpsub  20066  ogrpaddltbi  20068  ogrpaddltrd  20069  ogrpinv0lt  20072  orngsqr  20799  ornglmulle  20800  orngrmulle  20801  ofldchr  21531  umgr2edg  29282  2pthfrgr  30359  isarchi3  33269  archirngz  33271  archiabllem1a  33273  archiabllem1b  33274  archiabllem2a  33276  archiabllem2c  33277  lineext  36270  brsegle2  36303  cvrcmp  39539  cvrcmp2  39540  atcvreq0  39570  cvlatexch3  39594  cvlcvr1  39595  cvlsupr2  39599  cvlsupr7  39604  atnlej1  39635  atnlej2  39636  cvrval3  39669  ltltncvr  39679  atcvrneN  39686  atcvrj2b  39688  atbtwnex  39704  3noncolr2  39705  3noncolr1N  39706  4noncolr3  39709  3dimlem2  39715  3dimlem3a  39716  3dimlem3  39717  3dimlem3OLDN  39718  3dimlem4a  39719  3dimlem4  39720  3dimlem4OLDN  39721  ps-1  39733  hlatexch4  39737  3atlem1  39739  3atlem2  39740  3atlem3  39741  3atlem4  39742  3atlem5  39743  3atlem6  39744  3atlem7  39745  2llnmat  39780  ps-2c  39784  lplnri3N  39811  lplnexllnN  39820  2llnmeqat  39827  4atlem0a  39849  4atlem0ae  39850  4atlem0be  39851  4atlem9  39859  4atlem10a  39860  4atlem10b  39861  4atlem10  39862  4atlem11a  39863  4atlem11  39865  4atlem12a  39866  dalemcnes  39906  dalempnes  39907  dalemqnet  39908  dalem1  39915  dalemdea  39918  dalem3  39920  dalem5  39923  dalem-cly  39927  dalem27  39955  dalem28  39956  dalem41  39969  dalem45  39973  dalem48  39976  lneq2at  40034  2lnat  40040  2llnma1  40043  2llnma3r  40044  2llnma2  40045  cdlemblem  40049  paddasslem2  40077  pmodl42N  40107  hlmod1i  40112  atmod1i1m  40114  atmod2i1  40117  atmod2i2  40118  atmod3i1  40120  llnexchb2lem  40124  dalawlem2  40128  dalawlem3  40129  dalawlem6  40132  dalawlem7  40133  dalawlem11  40137  dalawlem12  40138  pexmidlem3N  40228  lhpexle3lem  40267  lhpmcvr3  40281  lhp2at0  40288  lhpelim  40293  lhpmod2i2  40294  lhpmod6i1  40295  4atexlempns  40318  4atexlemunv  40322  4atexlemc  40325  4atexlemnclw  40326  4atexlemex2  40327  4atexlemex6  40330  4atex  40332  4atex3  40337  trljat1  40422  trljat2  40423  ltrnatlw  40439  trlval4  40444  cdlemc1  40447  cdlemc3  40449  cdlemc6  40452  cdlemd3  40456  cdlemd4  40457  cdlemd5  40458  cdlemd6  40459  cdlemd7  40460  cdleme00a  40465  cdleme0cp  40470  cdleme0cq  40471  cdleme0e  40473  cdleme02N  40478  cdleme0ex2N  40480  cdleme0moN  40481  cdleme1  40483  cdleme2  40484  cdleme3e  40488  cdleme3g  40490  cdleme3h  40491  cdleme4  40494  cdleme5  40496  cdleme7aa  40498  cdleme7c  40501  cdleme7d  40502  cdleme7e  40503  cdleme8  40506  cdleme9  40509  cdleme10  40510  cdleme16aN  40515  cdleme11a  40516  cdleme11c  40517  cdleme11dN  40518  cdleme11e  40519  cdleme11g  40521  cdleme11h  40522  cdleme11j  40523  cdleme11k  40524  cdleme12  40527  cdleme15a  40530  cdleme15b  40531  cdleme16b  40535  cdleme17c  40544  cdleme0nex  40546  cdleme18d  40551  cdlemednpq  40555  cdleme20zN  40557  cdleme20y  40558  cdleme19a  40559  cdleme19d  40562  cdleme20aN  40565  cdleme20c  40567  cdleme20i  40573  cdleme20j  40574  cdleme21a  40581  cdleme21b  40582  cdleme21c  40583  cdleme21ct  40585  cdleme22cN  40598  cdleme22d  40599  cdleme22e  40600  cdleme22eALTN  40601  cdleme22f  40602  cdleme22f2  40603  cdleme22g  40604  cdleme23c  40607  cdleme41sn3a  40689  cdleme32le  40703  cdleme35b  40706  cdleme35c  40707  cdleme35d  40708  cdleme35e  40709  cdleme36a  40716  cdleme37m  40718  cdleme39a  40721  cdleme42a  40727  cdleme17d2  40751  cdlemeg46frv  40781  cdlemeg46rgv  40784  cdlemf1  40817  cdlemg2fv2  40856  cdlemg2l  40859  cdlemg2m  40860  cdlemg4d  40869  cdlemg4e  40870  cdlemg4f  40871  cdlemg4  40873  cdlemg6c  40876  cdlemg9a  40888  cdlemg10bALTN  40892  cdlemg12a  40899  cdlemg13  40908  cdlemg14f  40909  cdlemg14g  40910  cdlemg17i  40925  cdlemg17pq  40928  cdlemg19  40940  cdlemg21  40942  cdlemg27b  40952  cdlemg33c  40964  cdlemg33d  40965  trlcoabs2N  40978  cdlemg43  40986  cdlemg44b  40988  cdlemg44  40989  cdlemh1  41071  cdlemh2  41072  cdlemi1  41074  tendo0mul  41082  tendo0mulr  41083  cdlemk4  41090  cdlemk9  41095  cdlemk9bN  41096  cdlemk14  41110  cdlemkfid1N  41177  cdlemkid1  41178  cdlemk35s-id  41194  cdlemk39s-id  41196  cdlemk55a  41215  cdlemk55u  41222  cdlemk39u  41224  cdlemk19u  41226  cdlemk56  41227  cdleml8  41239  dia2dimlem1  41320  dia2dimlem2  41321  dia2dimlem3  41322  cdlemn10  41462  dihjust  41473  dihord1  41474  dihlsscpre  41490  dihvalcqpre  41491  dihglbcpreN  41556  dihmeetlem5  41564  dihmeetlem7N  41566  dihjatc1  41567  modmknepk  47604  modm2nep1  47608  modp2nep1  47609  modm1nep2  47610  modm1nem2  47611  lincreslvec3  48724  isldepslvec2  48727