Theorem syl131anc 1382

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 1127	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃 ∧ 𝜏))
6		syl23anc.5	. 2 ⊢ (𝜑 → 𝜂)
7		syl131anc.6	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁)
8	1, 5, 6, 7	syl3anc 1370	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 206  df-an 397  df-3an 1088

This theorem is referenced by:  syl132anc  1387  syl231anc  1389  syl133anc  1392  initoeu2lem1  17738  estrres  17865  mulgdir  18744  umgr2edg  27585  2pthfrgr  28657  omndadd2d  31343  omndadd2rd  31344  submomnd  31345  omndmul2  31347  omndmul3  31348  ogrpinv0le  31350  ogrpsub  31351  ogrpaddltbi  31353  ogrpaddltrd  31354  ogrpinv0lt  31357  isarchi3  31450  archirngz  31452  archiabllem1a  31454  archiabllem1b  31455  archiabllem2a  31457  archiabllem2c  31458  orngsqr  31512  ornglmulle  31513  orngrmulle  31514  ofldchr  31522  lineext  34387  brsegle2  34420  cvrcmp  37304  cvrcmp2  37305  atcvreq0  37335  cvlatexch3  37359  cvlcvr1  37360  cvlsupr2  37364  cvlsupr7  37369  atnlej1  37400  atnlej2  37401  cvrval3  37434  ltltncvr  37444  atcvrneN  37451  atcvrj2b  37453  atbtwnex  37469  3noncolr2  37470  3noncolr1N  37471  4noncolr3  37474  3dimlem2  37480  3dimlem3a  37481  3dimlem3  37482  3dimlem3OLDN  37483  3dimlem4a  37484  3dimlem4  37485  3dimlem4OLDN  37486  ps-1  37498  hlatexch4  37502  3atlem1  37504  3atlem2  37505  3atlem3  37506  3atlem4  37507  3atlem5  37508  3atlem6  37509  3atlem7  37510  2llnmat  37545  ps-2c  37549  lplnri3N  37576  lplnexllnN  37585  2llnmeqat  37592  4atlem0a  37614  4atlem0ae  37615  4atlem0be  37616  4atlem9  37624  4atlem10a  37625  4atlem10b  37626  4atlem10  37627  4atlem11a  37628  4atlem11  37630  4atlem12a  37631  dalemcnes  37671  dalempnes  37672  dalemqnet  37673  dalem1  37680  dalemdea  37683  dalem3  37685  dalem5  37688  dalem-cly  37692  dalem27  37720  dalem28  37721  dalem41  37734  dalem45  37738  dalem48  37741  lneq2at  37799  2lnat  37805  2llnma1  37808  2llnma3r  37809  2llnma2  37810  cdlemblem  37814  paddasslem2  37842  pmodl42N  37872  hlmod1i  37877  atmod1i1m  37879  atmod2i1  37882  atmod2i2  37883  atmod3i1  37885  llnexchb2lem  37889  dalawlem2  37893  dalawlem3  37894  dalawlem6  37897  dalawlem7  37898  dalawlem11  37902  dalawlem12  37903  pexmidlem3N  37993  lhpexle3lem  38032  lhpmcvr3  38046  lhp2at0  38053  lhpelim  38058  lhpmod2i2  38059  lhpmod6i1  38060  4atexlempns  38083  4atexlemunv  38087  4atexlemc  38090  4atexlemnclw  38091  4atexlemex2  38092  4atexlemex6  38095  4atex  38097  4atex3  38102  trljat1  38187  trljat2  38188  ltrnatlw  38204  trlval4  38209  cdlemc1  38212  cdlemc3  38214  cdlemc6  38217  cdlemd3  38221  cdlemd4  38222  cdlemd5  38223  cdlemd6  38224  cdlemd7  38225  cdleme00a  38230  cdleme0cp  38235  cdleme0cq  38236  cdleme0e  38238  cdleme02N  38243  cdleme0ex2N  38245  cdleme0moN  38246  cdleme1  38248  cdleme2  38249  cdleme3e  38253  cdleme3g  38255  cdleme3h  38256  cdleme4  38259  cdleme5  38261  cdleme7aa  38263  cdleme7c  38266  cdleme7d  38267  cdleme7e  38268  cdleme8  38271  cdleme9  38274  cdleme10  38275  cdleme16aN  38280  cdleme11a  38281  cdleme11c  38282  cdleme11dN  38283  cdleme11e  38284  cdleme11g  38286  cdleme11h  38287  cdleme11j  38288  cdleme11k  38289  cdleme12  38292  cdleme15a  38295  cdleme15b  38296  cdleme16b  38300  cdleme17c  38309  cdleme0nex  38311  cdleme18d  38316  cdlemednpq  38320  cdleme20zN  38322  cdleme20y  38323  cdleme19a  38324  cdleme19d  38327  cdleme20aN  38330  cdleme20c  38332  cdleme20i  38338  cdleme20j  38339  cdleme21a  38346  cdleme21b  38347  cdleme21c  38348  cdleme21ct  38350  cdleme22cN  38363  cdleme22d  38364  cdleme22e  38365  cdleme22eALTN  38366  cdleme22f  38367  cdleme22f2  38368  cdleme22g  38369  cdleme23c  38372  cdleme41sn3a  38454  cdleme32le  38468  cdleme35b  38471  cdleme35c  38472  cdleme35d  38473  cdleme35e  38474  cdleme36a  38481  cdleme37m  38483  cdleme39a  38486  cdleme42a  38492  cdleme17d2  38516  cdlemeg46frv  38546  cdlemeg46rgv  38549  cdlemf1  38582  cdlemg2fv2  38621  cdlemg2l  38624  cdlemg2m  38625  cdlemg4d  38634  cdlemg4e  38635  cdlemg4f  38636  cdlemg4  38638  cdlemg6c  38641  cdlemg9a  38653  cdlemg10bALTN  38657  cdlemg12a  38664  cdlemg13  38673  cdlemg14f  38674  cdlemg14g  38675  cdlemg17i  38690  cdlemg17pq  38693  cdlemg19  38705  cdlemg21  38707  cdlemg27b  38717  cdlemg33c  38729  cdlemg33d  38730  trlcoabs2N  38743  cdlemg43  38751  cdlemg44b  38753  cdlemg44  38754  cdlemh1  38836  cdlemh2  38837  cdlemi1  38839  tendo0mul  38847  tendo0mulr  38848  cdlemk4  38855  cdlemk9  38860  cdlemk9bN  38861  cdlemk14  38875  cdlemkfid1N  38942  cdlemkid1  38943  cdlemk35s-id  38959  cdlemk39s-id  38961  cdlemk55a  38980  cdlemk55u  38987  cdlemk39u  38989  cdlemk19u  38991  cdlemk56  38992  cdleml8  39004  dia2dimlem1  39085  dia2dimlem2  39086  dia2dimlem3  39087  cdlemn10  39227  dihjust  39238  dihord1  39239  dihlsscpre  39255  dihvalcqpre  39256  dihglbcpreN  39321  dihmeetlem5  39329  dihmeetlem7N  39331  dihjatc1  39332  lincreslvec3  45834  isldepslvec2  45837