MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl131anc Structured version   Visualization version   Unicode version

Theorem syl131anc 1305
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
syl12anc.1  |-  ( ph  ->  ps )
syl12anc.2  |-  ( ph  ->  ch )
syl12anc.3  |-  ( ph  ->  th )
syl22anc.4  |-  ( ph  ->  ta )
syl23anc.5  |-  ( ph  ->  et )
syl131anc.6  |-  ( ( ps  /\  ( ch 
/\  th  /\  ta )  /\  et )  ->  ze )
Assertion
Ref Expression
syl131anc  |-  ( ph  ->  ze )

Proof of Theorem syl131anc
StepHypRef Expression
1 syl12anc.1 . 2  |-  ( ph  ->  ps )
2 syl12anc.2 . . 3  |-  ( ph  ->  ch )
3 syl12anc.3 . . 3  |-  ( ph  ->  th )
4 syl22anc.4 . . 3  |-  ( ph  ->  ta )
52, 3, 43jca 1210 . 2  |-  ( ph  ->  ( ch  /\  th  /\  ta ) )
6 syl23anc.5 . 2  |-  ( ph  ->  et )
7 syl131anc.6 . 2  |-  ( ( ps  /\  ( ch 
/\  th  /\  ta )  /\  et )  ->  ze )
81, 5, 6, 7syl3anc 1292 1  |-  ( ph  ->  ze )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 1007
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 190  df-an 378  df-3an 1009
This theorem is referenced by:  syl132anc  1310  syl231anc  1312  syl133anc  1315  initoeu2lem1  15987  estrres  16102  mulgdir  16861  3v3e3cycl2  25471  omndadd2d  28545  omndadd2rd  28546  submomnd  28547  omndmul2  28549  omndmul3  28550  ogrpinvOLD  28552  ogrpinv0le  28553  ogrpsub  28554  ogrpaddltbi  28556  ogrpaddltrd  28557  ogrpinv0lt  28560  isarchi3  28578  archirngz  28580  archiabllem1a  28582  archiabllem1b  28583  archiabllem2a  28585  archiabllem2c  28586  orngsqr  28641  ornglmulle  28642  orngrmulle  28643  ofldchr  28651  lineext  30914  brsegle2  30947  cvrcmp  32920  cvrcmp2  32921  atcvreq0  32951  cvlatexch3  32975  cvlcvr1  32976  cvlsupr2  32980  cvlsupr7  32985  atnlej1  33015  atnlej2  33016  cvrval3  33049  ltltncvr  33059  atcvrneN  33066  atcvrj2b  33068  atbtwnex  33084  3noncolr2  33085  3noncolr1N  33086  4noncolr3  33089  3dimlem2  33095  3dimlem3a  33096  3dimlem3  33097  3dimlem3OLDN  33098  3dimlem4a  33099  3dimlem4  33100  3dimlem4OLDN  33101  ps-1  33113  hlatexch4  33117  3atlem1  33119  3atlem2  33120  3atlem3  33121  3atlem4  33122  3atlem5  33123  3atlem6  33124  3atlem7  33125  2llnmat  33160  ps-2c  33164  lplnri3N  33191  lplnexllnN  33200  2llnmeqat  33207  4atlem0a  33229  4atlem0ae  33230  4atlem0be  33231  4atlem9  33239  4atlem10a  33240  4atlem10b  33241  4atlem10  33242  4atlem11a  33243  4atlem11  33245  4atlem12a  33246  dalemcnes  33286  dalempnes  33287  dalemqnet  33288  dalem1  33295  dalemdea  33298  dalem3  33300  dalem5  33303  dalem-cly  33307  dalem27  33335  dalem28  33336  dalem41  33349  dalem45  33353  dalem48  33356  lneq2at  33414  2lnat  33420  2llnma1  33423  2llnma3r  33424  2llnma2  33425  cdlemblem  33429  paddasslem2  33457  pmodl42N  33487  hlmod1i  33492  atmod1i1m  33494  atmod2i1  33497  atmod2i2  33498  atmod3i1  33500  llnexchb2lem  33504  dalawlem2  33508  dalawlem3  33509  dalawlem6  33512  dalawlem7  33513  dalawlem11  33517  dalawlem12  33518  pexmidlem3N  33608  lhpexle3lem  33647  lhpmcvr3  33661  lhp2at0  33668  lhpelim  33673  lhpmod2i2  33674  lhpmod6i1  33675  4atexlempns  33698  4atexlemunv  33702  4atexlemc  33705  4atexlemnclw  33706  4atexlemex2  33707  4atexlemex6  33710  4atex  33712  4atex3  33717  trljat1  33803  trljat2  33804  ltrnatlw  33820  trlval4  33825  cdlemc1  33828  cdlemc3  33830  cdlemc6  33833  cdlemd3  33837  cdlemd4  33838  cdlemd5  33839  cdlemd6  33840  cdlemd7  33841  cdleme00a  33846  cdleme0cp  33851  cdleme0cq  33852  cdleme0e  33854  cdleme02N  33859  cdleme0ex2N  33861  cdleme0moN  33862  cdleme1  33864  cdleme2  33865  cdleme3e  33869  cdleme3g  33871  cdleme3h  33872  cdleme4  33875  cdleme5  33877  cdleme7aa  33879  cdleme7c  33882  cdleme7d  33883  cdleme7e  33884  cdleme8  33887  cdleme9  33890  cdleme10  33891  cdleme16aN  33896  cdleme11a  33897  cdleme11c  33898  cdleme11dN  33899  cdleme11e  33900  cdleme11g  33902  cdleme11h  33903  cdleme11j  33904  cdleme11k  33905  cdleme12  33908  cdleme15a  33911  cdleme15b  33912  cdleme16b  33916  cdleme17c  33925  cdleme0nex  33927  cdleme18d  33932  cdlemednpq  33936  cdleme20zN  33938  cdleme20y  33939  cdleme20yOLD  33940  cdleme19a  33941  cdleme19d  33944  cdleme20aN  33947  cdleme20c  33949  cdleme20i  33955  cdleme20j  33956  cdleme21a  33963  cdleme21b  33964  cdleme21c  33965  cdleme21ct  33967  cdleme22cN  33980  cdleme22d  33981  cdleme22e  33982  cdleme22eALTN  33983  cdleme22f  33984  cdleme22f2  33985  cdleme22g  33986  cdleme23c  33989  cdleme41sn3a  34071  cdleme32le  34085  cdleme35b  34088  cdleme35c  34089  cdleme35d  34090  cdleme35e  34091  cdleme36a  34098  cdleme37m  34100  cdleme39a  34103  cdleme42a  34109  cdleme17d2  34133  cdlemeg46frv  34163  cdlemeg46rgv  34166  cdlemf1  34199  cdlemg2fv2  34238  cdlemg2l  34241  cdlemg2m  34242  cdlemg4d  34251  cdlemg4e  34252  cdlemg4f  34253  cdlemg4  34255  cdlemg6c  34258  cdlemg9a  34270  cdlemg10bALTN  34274  cdlemg12a  34281  cdlemg13  34290  cdlemg14f  34291  cdlemg14g  34292  cdlemg17i  34307  cdlemg17pq  34310  cdlemg19  34322  cdlemg21  34324  cdlemg27b  34334  cdlemg33c  34346  cdlemg33d  34347  trlcoabs2N  34360  cdlemg43  34368  cdlemg44b  34370  cdlemg44  34371  cdlemh1  34453  cdlemh2  34454  cdlemi1  34456  tendo0mul  34464  tendo0mulr  34465  cdlemk4  34472  cdlemk9  34477  cdlemk9bN  34478  cdlemk14  34492  cdlemkfid1N  34559  cdlemkid1  34560  cdlemk35s-id  34576  cdlemk39s-id  34578  cdlemk55a  34597  cdlemk55u  34604  cdlemk39u  34606  cdlemk19u  34608  cdlemk56  34609  cdleml8  34621  dia2dimlem1  34703  dia2dimlem2  34704  dia2dimlem3  34705  cdlemn10  34845  dihjust  34856  dihord1  34857  dihlsscpre  34873  dihvalcqpre  34874  dihglbcpreN  34939  dihmeetlem5  34947  dihmeetlem7N  34949  dihjatc1  34950  lincreslvec3  40783  isldepslvec2  40786
  Copyright terms: Public domain W3C validator