Theorem syl131anc 1406

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 1103

This theorem is referenced by:  syl132anc  1411  syl231anc  1413  syl133anc  1416  initoeu2lem1  18061  estrres  18185  mulgdir  19163  omndadd2d  20191  omndadd2rd  20192  submomnd  20193  omndmul2  20194  omndmul3  20195  ogrpinv0le  20197  ogrpsub  20198  ogrpaddltbi  20200  ogrpaddltrd  20201  ogrpinv0lt  20204  orngsqr  20938  ornglmulle  20939  orngrmulle  20940  ofldchr  21686  umgr2edg  29468  2pthfrgr  30544  isarchi3  33420  archirngz  33422  archiabllem1a  33424  archiabllem1b  33425  archiabllem2a  33427  archiabllem2c  33428  lineext  36439  brsegle2  36472  cvrcmp  39919  cvrcmp2  39920  atcvreq0  39950  cvlatexch3  39974  cvlcvr1  39975  cvlsupr2  39979  cvlsupr7  39984  atnlej1  40015  atnlej2  40016  cvrval3  40049  ltltncvr  40059  atcvrneN  40066  atcvrj2b  40068  atbtwnex  40084  3noncolr2  40085  3noncolr1N  40086  4noncolr3  40089  3dimlem2  40095  3dimlem3a  40096  3dimlem3  40097  3dimlem3OLDN  40098  3dimlem4a  40099  3dimlem4  40100  3dimlem4OLDN  40101  ps-1  40113  hlatexch4  40117  3atlem1  40119  3atlem2  40120  3atlem3  40121  3atlem4  40122  3atlem5  40123  3atlem6  40124  3atlem7  40125  2llnmat  40160  ps-2c  40164  lplnri3N  40191  lplnexllnN  40200  2llnmeqat  40207  4atlem0a  40229  4atlem0ae  40230  4atlem0be  40231  4atlem9  40239  4atlem10a  40240  4atlem10b  40241  4atlem10  40242  4atlem11a  40243  4atlem11  40245  4atlem12a  40246  dalemcnes  40286  dalempnes  40287  dalemqnet  40288  dalem1  40295  dalemdea  40298  dalem3  40300  dalem5  40303  dalem-cly  40307  dalem27  40335  dalem28  40336  dalem41  40349  dalem45  40353  dalem48  40356  lneq2at  40414  2lnat  40420  2llnma1  40423  2llnma3r  40424  2llnma2  40425  cdlemblem  40429  paddasslem2  40457  pmodl42N  40487  hlmod1i  40492  atmod1i1m  40494  atmod2i1  40497  atmod2i2  40498  atmod3i1  40500  llnexchb2lem  40504  dalawlem2  40508  dalawlem3  40509  dalawlem6  40512  dalawlem7  40513  dalawlem11  40517  dalawlem12  40518  pexmidlem3N  40608  lhpexle3lem  40647  lhpmcvr3  40661  lhp2at0  40668  lhpelim  40673  lhpmod2i2  40674  lhpmod6i1  40675  4atexlempns  40698  4atexlemunv  40702  4atexlemc  40705  4atexlemnclw  40706  4atexlemex2  40707  4atexlemex6  40710  4atex  40712  4atex3  40717  trljat1  40802  trljat2  40803  ltrnatlw  40819  trlval4  40824  cdlemc1  40827  cdlemc3  40829  cdlemc6  40832  cdlemd3  40836  cdlemd4  40837  cdlemd5  40838  cdlemd6  40839  cdlemd7  40840  cdleme00a  40845  cdleme0cp  40850  cdleme0cq  40851  cdleme0e  40853  cdleme02N  40858  cdleme0ex2N  40860  cdleme0moN  40861  cdleme1  40863  cdleme2  40864  cdleme3e  40868  cdleme3g  40870  cdleme3h  40871  cdleme4  40874  cdleme5  40876  cdleme7aa  40878  cdleme7c  40881  cdleme7d  40882  cdleme7e  40883  cdleme8  40886  cdleme9  40889  cdleme10  40890  cdleme16aN  40895  cdleme11a  40896  cdleme11c  40897  cdleme11dN  40898  cdleme11e  40899  cdleme11g  40901  cdleme11h  40902  cdleme11j  40903  cdleme11k  40904  cdleme12  40907  cdleme15a  40910  cdleme15b  40911  cdleme16b  40915  cdleme17c  40924  cdleme0nex  40926  cdleme18d  40931  cdlemednpq  40935  cdleme20zN  40937  cdleme20y  40938  cdleme19a  40939  cdleme19d  40942  cdleme20aN  40945  cdleme20c  40947  cdleme20i  40953  cdleme20j  40954  cdleme21a  40961  cdleme21b  40962  cdleme21c  40963  cdleme21ct  40965  cdleme22cN  40978  cdleme22d  40979  cdleme22e  40980  cdleme22eALTN  40981  cdleme22f  40982  cdleme22f2  40983  cdleme22g  40984  cdleme23c  40987  cdleme41sn3a  41069  cdleme32le  41083  cdleme35b  41086  cdleme35c  41087  cdleme35d  41088  cdleme35e  41089  cdleme36a  41096  cdleme37m  41098  cdleme39a  41101  cdleme42a  41107  cdleme17d2  41131  cdlemeg46frv  41161  cdlemeg46rgv  41164  cdlemf1  41197  cdlemg2fv2  41236  cdlemg2l  41239  cdlemg2m  41240  cdlemg4d  41249  cdlemg4e  41250  cdlemg4f  41251  cdlemg4  41253  cdlemg6c  41256  cdlemg9a  41268  cdlemg10bALTN  41272  cdlemg12a  41279  cdlemg13  41288  cdlemg14f  41289  cdlemg14g  41290  cdlemg17i  41305  cdlemg17pq  41308  cdlemg19  41320  cdlemg21  41322  cdlemg27b  41332  cdlemg33c  41344  cdlemg33d  41345  trlcoabs2N  41358  cdlemg43  41366  cdlemg44b  41368  cdlemg44  41369  cdlemh1  41451  cdlemh2  41452  cdlemi1  41454  tendo0mul  41462  tendo0mulr  41463  cdlemk4  41470  cdlemk9  41475  cdlemk9bN  41476  cdlemk14  41490  cdlemkfid1N  41557  cdlemkid1  41558  cdlemk35s-id  41574  cdlemk39s-id  41576  cdlemk55a  41595  cdlemk55u  41602  cdlemk39u  41604  cdlemk19u  41606  cdlemk56  41607  cdleml8  41619  dia2dimlem1  41700  dia2dimlem2  41701  dia2dimlem3  41702  cdlemn10  41842  dihjust  41853  dihord1  41854  dihlsscpre  41870  dihvalcqpre  41871  dihglbcpreN  41936  dihmeetlem5  41944  dihmeetlem7N  41946  dihjatc1  41947  modmknepk  47960  modm2nep1  47964  modp2nep1  47965  modm1nep2  47966  modm1nem2  47967  lincreslvec3  49113  isldepslvec2  49116