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

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

Proof of Theorem simpr2
StepHypRef Expression
1 simp2 1055 . 2 ((𝜓𝜒𝜃) → 𝜒)
21adantl 481 1 ((𝜑 ∧ (𝜓𝜒𝜃)) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1031
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 196  df-an 385  df-3an 1033
This theorem is referenced by:  simplr2  1097  simprr2  1103  simp1r2  1151  simp2r2  1157  simp3r2  1163  3anandis  1426  fpr2g  6358  isopolem  6473  fr3nr  6849  frfi  8068  intrnfi  8183  fisupcl  8236  cnfcomlem  8457  ackbij1lem15  8917  cofsmo  8952  sornom  8960  fpwwe2lem5  9313  dedekindle  10053  supmul1  10842  eluzuzle  11531  xlesubadd  11925  elioc2  12066  elico2  12067  elicc2  12068  fseq1p1m1  12241  fz0fzelfz0  12272  swrdsbslen  13249  swrdspsleq  13250  ccatswrd  13257  swrdswrdlem  13260  tanadd  14685  dvds2ln  14801  cshwsidrepsw  15587  ressress  15714  f1ovscpbl  15958  mreexexlem4d  16079  mreexexd  16080  mreexexdOLD  16081  iscatd2  16114  2oppccomf  16157  issubc3  16281  fthmon  16359  fuccocl  16396  fucidcl  16397  invfuc  16406  initoeu2lem0  16435  initoeu2lem1  16436  curf2cl  16643  yonedalem4c  16689  yonedalem3  16692  pospo  16745  latjle12  16834  latjlej1  16837  latnlej2  16843  latlem12  16850  latmlem1  16853  latledi  16861  latjass  16867  latj12  16868  latj32  16869  latj13  16870  latj31  16871  latjrot  16872  latjjdi  16875  latjjdir  16876  latdisdlem  16961  prdsmndd  17095  frmdmnd  17168  grpsubrcan  17268  grpsubadd  17275  grpaddsubass  17277  grpsubsub4  17280  grppnpcan2  17281  grpnpncan  17282  mulgnndir  17341  mulgnndirOLD  17342  mulgnn0dir  17343  mulgdir  17345  mulgnnass  17348  mulgnnassOLD  17349  mulgnn0ass  17350  mulgass  17351  mulgsubdir  17354  pwsmulg  17359  issubg2  17381  eqgval  17415  qusgrp  17421  galcan  17509  gacan  17510  oppgmnd  17556  symggrp  17592  fvcosymgeq  17621  pmtrprfv  17645  psgnunilem3  17688  cmn32  17983  cmn12  17985  abladdsub  17992  ablsubsub23  18002  mulgdi  18004  mulgsubdi  18007  dprdss  18200  dprdz  18201  dprdf1o  18203  dprdsn  18207  dprd2da  18213  dmdprdsplit  18218  ablfac1b  18241  pgpfac1lem5  18250  srgi  18283  srgbinom  18317  ringi  18332  prdsringd  18384  opprring  18403  mulgass3  18409  dvrass  18462  subrgunit  18570  issubrg2  18572  abvdiv  18609  lsssn0  18718  islss3  18729  prdslmodd  18739  islmhm2  18808  lspsolv  18913  islbs2  18924  islbs3  18925  lbsextlem4  18931  sralmod  18957  issubassa  19094  sraassa  19095  psrbaglesupp  19138  psrbaglecl  19139  psrbagcon  19141  psrgrp  19168  psrlmod  19171  psrring  19181  psrassa  19184  psgndiflemB  19713  ipdir  19751  ipdi  19752  ipsubdir  19754  ipsubdi  19755  ipass  19757  ipassr  19758  ipassr2  19759  isphld  19766  ocvlss  19783  mamudm  19961  matring  20016  matassa  20017  ofco2  20024  ma1repveval  20144  mdetunilem1  20185  mdetunilem9  20193  chpscmatgsumbin  20416  iinopn  20480  restopnb  20737  subbascn  20816  nrmsep2  20918  isnrm3  20921  regsep2  20938  dnsconst  20940  dfcon2  20980  1stcelcls  21022  dislly  21058  ptuni2  21137  tx1stc  21211  0nelfb  21393  infil  21425  fsubbas  21429  filssufilg  21473  hauspwpwf1  21549  cnextcn  21629  tmdcn2  21651  ustuqtoplem  21801  utopsnneiplem  21809  psmettri  21874  isxmet2d  21890  xmettri  21914  xmetres2  21924  bldisj  21961  blss2ps  21966  blss2  21967  xmstri2  22029  mstri2  22030  xmstri  22031  mstri  22032  xmstri3  22033  mstri3  22034  msrtri  22035  comet  22076  stdbdbl  22080  met2ndci  22085  ngprcan  22172  ngplcan  22173  ngpsubcan  22176  nmtri2  22189  nrgdsdi  22227  nrgdsdir  22228  nlmdsdi  22243  nlmdsdir  22244  blcvx  22357  icoopnst  22494  pi1grplem  22605  clmpm1dir  22659  cmodscmulexp  22678  cvsdiv  22688  cvsdivcl  22689  cphdivcl  22735  cphsubdir  22761  cphsubdi  22762  tchcph  22789  bcthlem5  22878  volfiniun  23067  volcn  23125  itg1val2  23202  dvconst  23431  dvlip  23505  ftc1a  23549  ulmval  23883  ulmdvlem3  23905  ang180  24289  cvxcl  24456  scvxcvx  24457  sgmmul  24671  dchrabl  24724  gausslemma2dlem1a  24835  motgrp  25184  iscgra1  25448  cgrane1  25450  cgrane3  25452  cgrahl1  25454  cgrahl2  25455  cgracgr  25456  cgratr  25461  cgrabtwn  25463  cgrahl  25464  dfcgra2  25467  sacgr  25468  f1otrge  25498  colinearalglem1  25532  axcgrtr  25541  axeuclidlem  25588  axcontlem3  25592  axcontlem4  25593  axcontlem7  25596  eengtrkg  25611  eengtrkge  25612  isspthonpth  25908  wlkdvspth  25932  clwlkfoclwwlk  26166  el2spthonot0  26192  el2wlkonotot0  26193  usg2wotspth  26205  2spontn0vne  26208  rusgranumwlks  26277  rusgranumwwlkg  26280  iseupa  26286  3vfriswmgra  26326  frgrareggt1  26437  grpomuldivass  26573  ablomuldiv  26584  ablodivdiv4  26586  ablonnncan1  26590  nvmdi  26681  dipassr  26879  archiabllem2c  28874  dvrdir  28915  dvrcan5  28918  reofld  28965  pstmfval  29061  qqhval2lem  29147  qqhvq  29153  measdivcstOLD  29408  measdivcst  29409  carsggect  29501  bnj1098  29902  bnj149  29993  bnj1118  30100  erdszelem9  30229  rescon  30276  cvmseu  30306  cvmlift2lem10  30342  cvmlift2lem12  30344  elmrsubrn  30465  mclsind  30515  frrlem4  30821  cgrid2  31074  segconeu  31082  btwncomim  31084  btwnswapid  31088  trisegint  31099  cgrxfr  31126  brofs2  31148  endofsegid  31156  btwnconn2  31173  seglemin  31184  segletr  31185  btwnsegle  31188  colinbtwnle  31189  broutsideof2  31193  btwnoutside  31196  broutsideof3  31197  outsideoftr  31200  outsidele  31203  fvray  31212  fvline  31215  ellines  31223  broucube  32407  ftc1anc  32457  sdclem1  32503  sstotbnd2  32537  iscringd  32761  lsmsat  33107  lfladdcl  33170  lflnegcl  33174  lflvscl  33176  eqlkr  33198  lshpkrlem4  33212  lshpkrlem6  33214  ldualgrplem  33244  lduallmodlem  33251  latmassOLD  33328  latm12  33329  latm32  33330  latmrot  33331  latmmdiN  33333  latmmdir  33334  omlfh1N  33357  omlfh3N  33358  cvrnbtwn2  33374  cvlexchb1  33429  cvlsupr2  33442  hlatjass  33468  hlatj12  33469  hlatj32  33470  cvrat  33520  cvrat2  33527  atltcvr  33533  atexchltN  33539  cvrat3  33540  cvrat4  33541  atbtwnexOLDN  33545  atbtwnex  33546  3dimlem3  33559  3dimlem3OLDN  33560  3at  33588  2atneat  33613  llncmp  33620  2at0mat0  33623  2atmat0  33624  llncvrlpln  33656  lplncmp  33660  2llnjaN  33664  4atlem11  33707  lplncvrlvol  33714  lvolcmp  33715  2atm2atN  33883  elpaddatriN  33901  paddasslem8  33925  paddass  33936  padd12N  33937  paddssw2  33942  paddss  33943  pmod1i  33946  pmodN  33948  pmapjlln1  33953  atmod1i1  33955  atmod1i2  33957  pexmidlem2N  34069  pl42lem2N  34078  pl42lem3N  34079  pl42lem4N  34080  pl42N  34081  lhpm0atN  34127  lautlt  34189  lautcvr  34190  lautj  34191  lautm  34192  ltrneq2  34246  cdlemd1  34297  cdleme1b  34325  cdleme1  34326  cdleme2  34327  cdleme3e  34331  cdlemefr27cl  34503  cdlemefs27cl  34513  cdleme42ke  34585  cdleme42mN  34587  cdlemf2  34662  cdlemftr2  34666  trljco  34840  tgrpgrplem  34849  tendoplass  34883  tendodi1  34884  tendodi2  34885  cdlemk34  35010  cdlemk36  35013  erngdvlem3-rN  35098  tendospdi1  35121  dialss  35147  dvhvaddass  35198  dvhopvsca  35203  dvhlveclem  35209  diblss  35271  diclss  35294  diclspsn  35295  cdlemn11pre  35311  dihmeetlem12N  35419  dihmeetlem16N  35423  dihmeetlem17N  35424  dihmeetlem18N  35425  dvh4dimN  35548  lpolconN  35588  dochpolN  35591  lclkr  35634  lclkrs  35640  lcfr  35686  irrapxlem6  36203  jm2.26lem3  36380  dgrsub2  36518  mpaaroot  36538  mendring  36575  mendlmod  36576  mendassa  36577  relexpmulg  36815  iunrelexpmin2  36817  relexpxpmin  36822  neicvgel1  37231  rfcnpre3  38009  fmuldfeq  38444  stoweidlem43  38730  stoweidlem52  38739  stoweidlem53  38740  stoweidlem56  38743  stoweidlem57  38744  stoweidlem60  38747  issmfle  39426  issmfgt  39437  issmfge  39450  smflimlem4  39454  iccpartigtl  39756  iccelpart  39766  ltsubsubaddltsub  40164  subgruhgredgd  40500  nbfusgrlevtxm2  40598  upgr1wlkwlk  40839  lfgriswlk  40889  1wlkiswwlksupgr2  41066  umgrwwlks2on  41153  rusgrnumwwlks  41169  3spthd  41335  3vfriswmgr  41440  frgr2wwlkeqm  41488  av-numclwwlk2  41529  av-numclwwlk3  41531  av-numclwwlk5  41534  copissgrp  41590  cznrng  41739  funcringcsetcALTV2lem9  41828  funcringcsetclem9ALTV  41851  ldepsprlem  42047  lincresunit3  42056  lincreslvec3  42057
  Copyright terms: Public domain W3C validator