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

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

Proof of Theorem simpr2
StepHypRef Expression
1 simp2 1082 . 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:  simplr2  1124  simprr2  1130  simp1r2  1178  simp2r2  1184  simp3r2  1190  3anandis  1474  fpr2g  6516  isopolem  6635  fr3nr  7021  frfi  8246  intrnfi  8363  fisupcl  8416  cnfcomlem  8634  ackbij1lem15  9094  cofsmo  9129  sornom  9137  fpwwe2lem5  9494  dedekindle  10239  supmul1  11030  eluzuzle  11734  xlesubadd  12131  elioc2  12274  elico2  12275  elicc2  12276  fseq1p1m1  12452  fz0fzelfz0  12484  swrdsbslen  13494  swrdspsleq  13495  ccatswrd  13502  swrdswrdlem  13505  tanadd  14941  dvds2ln  15061  cshwsidrepsw  15847  ressress  15985  f1ovscpbl  16233  mreexexlem4d  16354  mreexexd  16355  mreexexdOLD  16356  iscatd2  16389  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  latjass  17142  latj12  17143  latj32  17144  latj13  17145  latj31  17146  latjrot  17147  latjjdi  17150  latjjdir  17151  latdisdlem  17236  prdsmndd  17370  frmdmnd  17443  grpsubrcan  17543  grpsubadd  17550  grpaddsubass  17552  grpsubsub4  17555  grppnpcan2  17556  grpnpncan  17557  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  fvcosymgeq  17895  pmtrprfv  17919  psgnunilem3  17962  cmn32  18257  cmn12  18259  abladdsub  18266  ablsubsub23  18276  mulgdi  18278  mulgsubdi  18281  dprdss  18474  dprdz  18475  dprdf1o  18477  dprdsn  18481  dprd2da  18487  dmdprdsplit  18492  ablfac1b  18515  pgpfac1lem5  18524  srgi  18557  srgbinom  18591  ringi  18606  prdsringd  18658  opprring  18677  mulgass3  18683  dvrass  18736  subrgunit  18846  issubrg2  18848  abvdiv  18885  lsssn0  18996  islss3  19007  prdslmodd  19017  islmhm2  19086  lspsolv  19191  islbs2  19202  islbs3  19203  lbsextlem4  19209  sralmod  19235  issubassa  19372  sraassa  19373  psrbaglesupp  19416  psrbaglecl  19417  psrbagcon  19419  psrgrp  19446  psrlmod  19449  psrring  19459  psrassa  19462  psgndiflemB  19994  ipdir  20032  ipdi  20033  ipsubdir  20035  ipsubdi  20036  ipass  20038  ipassr  20039  ipassr2  20040  isphld  20047  ocvlss  20064  mamudm  20242  matring  20297  matassa  20298  ofco2  20305  ma1repveval  20425  mdetunilem1  20466  mdetunilem9  20474  chpscmatgsumbin  20697  iinopn  20755  restopnb  21027  subbascn  21106  nrmsep2  21208  isnrm3  21211  regsep2  21228  dnsconst  21230  dfconn2  21270  1stcelcls  21312  dislly  21348  ptuni2  21427  tx1stc  21501  0nelfb  21682  infil  21714  fsubbas  21718  filssufilg  21762  hauspwpwf1  21838  cnextcn  21918  tmdcn2  21940  ustuqtoplem  22090  utopsnneiplem  22098  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  icoopnst  22785  pi1grplem  22895  clmpm1dir  22949  cmodscmulexp  22968  cvsdiv  22978  cvsdivcl  22979  cphdivcl  23028  cphsubdir  23054  cphsubdi  23055  tchcph  23082  bcthlem5  23171  volfiniun  23361  volcn  23420  itg1val2  23496  dvconst  23725  dvlip  23801  ftc1a  23845  ulmval  24179  ulmdvlem3  24201  ang180  24589  cvxcl  24756  scvxcvx  24757  sgmmul  24971  dchrabl  25024  gausslemma2dlem1a  25135  motgrp  25483  iscgra1  25747  cgrane1  25749  cgrane3  25751  cgrahl1  25753  cgrahl2  25754  cgracgr  25755  cgratr  25760  cgrabtwn  25762  cgrahl  25763  dfcgra2  25766  sacgr  25767  f1otrge  25797  colinearalglem1  25831  axcgrtr  25840  axeuclidlem  25887  axcontlem3  25891  axcontlem4  25892  axcontlem7  25895  eengtrkg  25910  eengtrkge  25911  edglnl  26083  subgruhgredgd  26221  nbfusgrlevtxm2  26324  lfgriswlk  26641  wwlknbp1  26792  umgrwwlks2on  26923  rusgrnumwwlks  26941  3spthd  27154  3vfriswmgr  27258  frgr2wwlkeqm  27311  numclwlk1lem2f  27345  numclwwlk2  27361  numclwwlk2OLD  27368  numclwwlk3  27372  numclwwlk5  27375  grpomuldivass  27523  ablomuldiv  27534  ablodivdiv4  27536  ablonnncan1  27540  nvmdi  27631  dipassr  27829  archiabllem2c  29877  dvrdir  29918  dvrcan5  29921  reofld  29968  pstmfval  30067  qqhval2lem  30153  qqhvq  30159  measdivcstOLD  30415  measdivcst  30416  carsggect  30508  tgoldbachgtd  30868  bnj1098  30980  bnj149  31071  bnj1118  31178  erdszelem9  31307  resconn  31354  cvmseu  31384  cvmlift2lem10  31420  cvmlift2lem12  31422  elmrsubrn  31543  mclsind  31593  noprefixmo  31973  nosupbnd1  31985  ssltss2  32029  cgrid2  32235  segconeu  32243  btwncomim  32245  btwnswapid  32249  trisegint  32260  cgrxfr  32287  brofs2  32309  endofsegid  32317  btwnconn2  32334  seglemin  32345  segletr  32346  btwnsegle  32349  colinbtwnle  32350  broutsideof2  32354  btwnoutside  32357  broutsideof3  32358  outsideoftr  32361  outsidele  32364  fvray  32373  fvline  32376  ellines  32384  broucube  33573  ftc1anc  33623  sdclem1  33669  sstotbnd2  33703  iscringd  33927  lsmsat  34613  lfladdcl  34676  lflnegcl  34680  lflvscl  34682  eqlkr  34704  lshpkrlem4  34718  lshpkrlem6  34720  ldualgrplem  34750  lduallmodlem  34757  latmassOLD  34834  latm12  34835  latm32  34836  latmrot  34837  latmmdiN  34839  latmmdir  34840  omlfh1N  34863  omlfh3N  34864  cvrnbtwn2  34880  cvlexchb1  34935  cvlsupr2  34948  hlatjass  34974  hlatj12  34975  hlatj32  34976  cvrat  35026  cvrat2  35033  atltcvr  35039  atexchltN  35045  cvrat3  35046  cvrat4  35047  atbtwnexOLDN  35051  atbtwnex  35052  3dimlem3  35065  3dimlem3OLDN  35066  3at  35094  2atneat  35119  llncmp  35126  2at0mat0  35129  2atmat0  35130  llncvrlpln  35162  lplncmp  35166  2llnjaN  35170  4atlem11  35213  lplncvrlvol  35220  lvolcmp  35221  2atm2atN  35389  elpaddatriN  35407  paddasslem8  35431  paddass  35442  padd12N  35443  paddssw2  35448  paddss  35449  pmod1i  35452  pmodN  35454  pmapjlln1  35459  atmod1i1  35461  atmod1i2  35463  pexmidlem2N  35575  pl42lem2N  35584  pl42lem3N  35585  pl42lem4N  35586  pl42N  35587  lhpm0atN  35633  lautlt  35695  lautcvr  35696  lautj  35697  lautm  35698  ltrneq2  35752  cdlemd1  35803  cdleme1b  35831  cdleme1  35832  cdleme2  35833  cdleme3e  35837  cdlemefr27cl  36008  cdlemefs27cl  36018  cdleme42ke  36090  cdleme42mN  36092  cdlemf2  36167  cdlemftr2  36171  trljco  36345  tgrpgrplem  36354  tendoplass  36388  tendodi1  36389  tendodi2  36390  cdlemk34  36515  cdlemk36  36518  erngdvlem3-rN  36603  tendospdi1  36626  dialss  36652  dvhvaddass  36703  dvhopvsca  36708  dvhlveclem  36714  diblss  36776  diclss  36799  diclspsn  36800  cdlemn11pre  36816  dihmeetlem12N  36924  dihmeetlem16N  36928  dihmeetlem17N  36929  dihmeetlem18N  36930  dvh4dimN  37053  lpolconN  37093  dochpolN  37096  lclkr  37139  lclkrs  37145  lcfr  37191  irrapxlem6  37708  jm2.26lem3  37885  dgrsub2  38022  mpaaroot  38042  mendring  38079  mendlmod  38080  mendassa  38081  relexpmulg  38319  iunrelexpmin2  38321  relexpxpmin  38326  neicvgel1  38734  rfcnpre3  39506  fmuldfeq  40133  xlimbr  40371  stoweidlem43  40578  stoweidlem52  40587  stoweidlem53  40588  stoweidlem56  40591  stoweidlem57  40592  stoweidlem60  40595  issmfle  41275  issmfgt  41286  issmfge  41299  smflimlem4  41303  ltsubsubaddltsub  41640  iccpartigtl  41684  iccelpart  41694  upgrwlkupwlk  42046  copissgrp  42133  cznrng  42280  funcringcsetcALTV2lem9  42369  funcringcsetclem9ALTV  42392  ldepsprlem  42586  lincresunit3  42595  lincreslvec3  42596
  Copyright terms: Public domain W3C validator