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

Theorem simpr1 1087
Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
Assertion
Ref Expression
simpr1 ((𝜑 ∧ (𝜓𝜒𝜃)) → 𝜓)

Proof of Theorem simpr1
StepHypRef Expression
1 simp1 1081 . 2 ((𝜓𝜒𝜃) → 𝜓)
21adantl 481 1 ((𝜑 ∧ (𝜓𝜒𝜃)) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054
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 197  df-an 385  df-3an 1056
This theorem is referenced by:  simplr1  1123  simprr1  1129  simp1r1  1177  simp2r1  1183  simp3r1  1189  3anandis  1474  fpr2g  6516  isopolem  6635  fr3nr  7021  suppfnss  7365  frfi  8246  intrnfi  8363  iinfi  8364  eqsup  8403  fisupcl  8416  cnfcomlem  8634  ackbij1lem15  9094  fpwwe2lem5  9494  dedekindle  10239  ico0  12259  elioc2  12274  elico2  12275  elicc2  12276  iccsplit  12343  fseq1p1m1  12452  elfz0ubfz0  12482  hashtpg  13305  swrdsbslen  13494  swrdspsleq  13495  ccatswrd  13502  tanadd  14941  dvds2ln  15061  qredeq  15418  ressress  15985  mreexexlem4d  16354  mreexexd  16355  mreexexdOLD  16356  0catg  16395  2oppccomf  16432  issubc3  16556  fthmon  16634  fuccocl  16671  fucidcl  16672  invfuc  16681  initoeu2lem0  16710  initoeu2lem1  16711  curf2cl  16918  yonedalem4c  16964  yonedalem3  16967  pospo  17020  latjle12  17109  latjlej1  17112  latnlej2  17118  latlem12  17125  latmlem1  17128  latledi  17136  latmlej11  17137  latjass  17142  latj12  17143  latj32  17144  latj13  17145  latj31  17146  latjrot  17147  latjjdi  17150  latjjdir  17151  latdisdlem  17236  prdsmndd  17370  imasmnd2  17374  frmdmnd  17443  grpsubrcan  17543  grpsubadd  17550  grpsubsub  17551  grpaddsubass  17552  grpsubsub4  17555  grpnnncan2  17559  imasgrp2  17577  mulgnndir  17616  mulgnndirOLD  17617  mulgnn0dir  17618  mulgdir  17620  mulgnnass  17623  mulgnnassOLD  17624  mulgnn0ass  17625  mulgass  17626  mulgsubdir  17629  pwsmulg  17634  issubg2  17656  eqgval  17690  qusgrp  17696  galcan  17783  gacan  17784  oppgmnd  17830  symggrp  17866  pmtrprfv  17919  pmtr3ncom  17941  psgnunilem3  17962  cmn32  18257  cmn12  18259  abladdsub  18266  mulgnn0di  18277  mulgdi  18278  mulgsubdi  18281  dprdss  18474  dprdz  18475  dprdf1o  18477  dprdsn  18481  dprd2da  18487  ablfac1b  18515  pgpfac1lem5  18524  srgbinomlem2  18587  srgbinom  18591  ringi  18606  prdsringd  18658  imasring  18665  opprring  18677  mulgass3  18683  dvrass  18736  kerf1hrm  18791  subrgunit  18846  issubrg2  18848  abvdiv  18885  islss3  19007  prdslmodd  19017  islmhm2  19086  lspsolv  19191  islbs2  19202  islbs3  19203  lbsextlem4  19209  sralmod  19235  issubassa  19372  sraassa  19373  psrbaglecl  19417  psrbagcon  19419  psrgrp  19446  psrlmod  19449  psrring  19459  psrassa  19462  ipdir  20032  ipdi  20033  ipsubdir  20035  ipsubdi  20036  ipass  20038  ipassr  20039  ipassr2  20040  ocvlss  20064  mamudm  20242  matring  20297  matassa  20298  ofco2  20305  mdetunilem1  20466  mdetunilem9  20474  mdetuni0  20475  mdetmul  20477  gsummatr01lem3  20511  iinopn  20755  subbascn  21106  nrmsep2  21208  isnrm3  21211  regsep2  21228  dnsconst  21230  dfconn2  21270  1stcelcls  21312  nllyidm  21340  dislly  21348  upxp  21474  fbasne0  21681  filss  21704  infil  21714  fsubbas  21718  filssufilg  21762  tmdcn2  21940  psmettri  22163  isxmet2d  22179  xmettri  22203  xmetres2  22213  bldisj  22250  blss2ps  22255  blss2  22256  xmstri2  22318  mstri2  22319  xmstri  22320  mstri  22321  xmstri3  22322  mstri3  22323  msrtri  22324  comet  22365  stdbdbl  22369  met2ndci  22374  ngprcan  22461  ngplcan  22462  ngpsubcan  22465  nmtri2  22478  nrgdsdi  22516  nrgdsdir  22517  nlmdsdi  22532  nlmdsdir  22533  blcvx  22648  icccmplem2  22673  pi1grplem  22895  pi1cof  22905  clmpm1dir  22949  cvsdiv  22978  cvsdivcl  22979  cphdivcl  23028  cphsubdir  23054  cphsubdi  23055  cphassr  23058  bcthlem5  23171  rrxcph  23226  volfiniun  23361  volcn  23420  itg1val2  23496  dvconst  23725  dvlip  23801  dvfsumlem4  23837  ftc1a  23845  ulmval  24179  ulmdvlem3  24201  ang180  24589  cvxcl  24756  scvxcvx  24757  sgmmul  24971  logexprlim  24995  dchrabl  25024  motgrp  25483  iscgra1  25747  cgrane1  25749  cgrane2  25750  cgrahl1  25753  cgrahl2  25754  cgracgr  25755  cgratr  25760  cgrabtwn  25762  dfcgra2  25766  sacgr  25767  f1otrge  25797  colinearalglem1  25831  colinearalg  25835  axcgrtr  25840  axlowdimlem16  25882  axeuclidlem  25887  axcontlem7  25895  eengtrkg  25910  eengtrkge  25911  nbfusgrlevtxm2  26324  lfgriswlk  26641  upgrwlkdvde  26689  wwlknbp1  26792  erclwwlktr  26979  erclwwlkntr  27035  frgr2wwlkeqm  27311  numclwlk1lem2f  27345  numclwwlk5  27375  friendship  27386  grpodivdiv  27522  grpomuldivass  27523  ablodivdiv4  27536  ablonnncan  27538  ablonnncan1  27540  nvmdi  27631  dipassr  27829  archiabllem2c  29877  dvrdir  29918  dvrcan5  29921  reofld  29968  pstmfval  30067  tpr2rico  30086  qqhval2lem  30153  qqhvq  30159  issiga  30302  measdivcstOLD  30415  measdivcst  30416  carsggect  30508  signsply0  30756  tgoldbachgtd  30868  bnj149  31071  bnj1118  31178  bnj1128  31184  erdszelem9  31307  resconn  31354  cvmseu  31384  cvmlift2lem12  31422  elmrsubrn  31543  mclsind  31593  frrlem4  31908  frrlem11  31917  noprefixmo  31973  nosupbnd1  31985  ssltss1  32028  cgrid2  32235  segconeu  32243  btwncomim  32245  btwnswapid  32249  cgrxfr  32287  btwnxfr  32288  colineardim1  32293  brofs2  32309  brifs2  32310  idinside  32316  endofsegid  32317  btwnconn1lem7  32325  btwnconn1lem11  32329  btwnconn1  32333  segcon2  32337  seglemin  32345  segletr  32346  btwnsegle  32349  colinbtwnle  32350  broutsideof2  32354  broutsideof3  32358  outsidele  32364  fvray  32373  fvline  32376  linerflx1  32381  ellines  32384  ivthALT  32455  poimirlem32  33571  ftc1anc  33623  sdclem1  33669  sstotbnd2  33703  zerdivemp1x  33876  isdrngo2  33887  iscringd  33927  lsmsat  34613  lfladdcl  34676  lflnegcl  34680  lflvscl  34682  lshpkrlem4  34718  lshpkrlem6  34720  ldualgrplem  34750  lduallmodlem  34757  latmassOLD  34834  latm12  34835  latm32  34836  latmrot  34837  latmmdiN  34839  latmmdir  34840  omlfh1N  34863  omlfh3N  34864  cvlexchb1  34935  cvlexch3  34937  cvlexch4N  34938  cvlatexchb1  34939  cvlsupr2  34948  hlatjass  34974  hlatj12  34975  hlatj32  34976  cvratlem  35025  cvrat  35026  atcvrj0  35032  cvrat2  35033  atltcvr  35039  atexchltN  35045  cvrat3  35046  cvrat4  35047  3dimlem3  35065  3dimlem3OLDN  35066  3at  35094  2atneat  35119  llncmp  35126  2at0mat0  35129  2atmat0  35130  lplnnle2at  35145  llncvrlpln  35162  lplncmp  35166  lplnexllnN  35168  2llnjaN  35170  4atlem11  35213  lplncvrlvol  35220  lvolcmp  35221  2atm2atN  35389  elpaddatriN  35407  paddasslem9  35432  paddass  35442  padd12N  35443  paddssw2  35448  paddss  35449  pmodlem2  35451  pmodN  35454  pmapjlln1  35459  atmod1i1  35461  atmod1i2  35463  pexmidlem2N  35575  pexmidlem6N  35579  pl42N  35587  lhpm0atN  35633  lautlt  35695  lautcvr  35696  lautj  35697  lautm  35698  ltrneq2  35752  cdlemc3  35798  cdlemc4  35799  cdlemd1  35803  cdleme1b  35831  cdleme1  35832  cdleme2  35833  cdleme3e  35837  cdlemefr27cl  36008  cdlemefs27cl  36018  cdleme42mN  36092  cdlemftr2  36171  trljco  36345  tgrpgrplem  36354  tendoplass  36388  tendodi1  36389  tendodi2  36390  cdlemk36  36518  erngdvlem3  36595  erngdvlem3-rN  36603  tendospdi1  36626  dvalveclem  36631  dialss  36652  dvhvaddass  36703  dvhopvsca  36708  dvhlveclem  36714  diblss  36776  diclss  36799  dihmeetlem12N  36924  dihmeetlem15N  36927  dihmeetlem16N  36928  dihmeetlem17N  36929  dihmeetlem18N  36930  dihmeetlem19N  36931  dvh4dimN  37053  lpolvN  37092  lclkr  37139  lclkrs  37145  lcfr  37191  irrapxlem6  37708  jm2.26lem3  37885  dgrsub2  38022  mpaadgr  38041  mendring  38079  mendlmod  38080  mendassa  38081  relexpmulg  38319  iunrelexpmin2  38321  relexpxpmin  38326  neicvgel1  38734  fmuldfeq  40133  stoweidlem43  40578  stoweidlem52  40587  stoweidlem53  40588  stoweidlem56  40591  stoweidlem57  40592  issmfle  41275  issmfgt  41286  issmfge  41299  fmtnoprmfac1  41802  fmtnoprmfac2  41804  upgrwlkupwlk  42046  copissgrp  42133  cznrng  42280  funcringcsetcALTV2lem9  42369  funcringcsetclem9ALTV  42392  ply1ass23l  42495  linccl  42528  lincext1  42568  lincext3  42570  lincresunit2  42592
  Copyright terms: Public domain W3C validator