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

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

Proof of Theorem simpr1
StepHypRef Expression
1 simp1 1059 . 2 ((𝜓𝜒𝜃) → 𝜓)
21adantl 482 1 ((𝜑 ∧ (𝜓𝜒𝜃)) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  simplr1  1101  simprr1  1107  simp1r1  1155  simp2r1  1161  simp3r1  1167  3anandis  1431  fpr2g  6429  isopolem  6549  fr3nr  6926  suppfnss  7265  frfi  8149  intrnfi  8266  iinfi  8267  eqsup  8306  fisupcl  8319  cnfcomlem  8540  ackbij1lem15  9000  fpwwe2lem5  9400  dedekindle  10145  ico0  12163  elioc2  12178  elico2  12179  elicc2  12180  iccsplit  12247  fseq1p1m1  12355  elfz0ubfz0  12384  hashtpg  13205  swrdsbslen  13386  swrdspsleq  13387  ccatswrd  13394  tanadd  14822  dvds2ln  14938  qredeq  15295  ressress  15859  mreexexlem4d  16228  mreexexd  16229  mreexexdOLD  16230  0catg  16269  2oppccomf  16306  issubc3  16430  fthmon  16508  fuccocl  16545  fucidcl  16546  invfuc  16555  initoeu2lem0  16584  initoeu2lem1  16585  curf2cl  16792  yonedalem4c  16838  yonedalem3  16841  pospo  16894  latjle12  16983  latjlej1  16986  latnlej2  16992  latlem12  16999  latmlem1  17002  latledi  17010  latmlej11  17011  latjass  17016  latj12  17017  latj32  17018  latj13  17019  latj31  17020  latjrot  17021  latjjdi  17024  latjjdir  17025  latdisdlem  17110  prdsmndd  17244  imasmnd2  17248  frmdmnd  17317  grpsubrcan  17417  grpsubadd  17424  grpsubsub  17425  grpaddsubass  17426  grpsubsub4  17429  grpnnncan2  17433  imasgrp2  17451  mulgnndir  17490  mulgnndirOLD  17491  mulgnn0dir  17492  mulgdir  17494  mulgnnass  17497  mulgnnassOLD  17498  mulgnn0ass  17499  mulgass  17500  mulgsubdir  17503  pwsmulg  17508  issubg2  17530  eqgval  17564  qusgrp  17570  galcan  17658  gacan  17659  oppgmnd  17705  symggrp  17741  pmtrprfv  17794  pmtr3ncom  17816  psgnunilem3  17837  cmn32  18132  cmn12  18134  abladdsub  18141  mulgnn0di  18152  mulgdi  18153  mulgsubdi  18156  dprdss  18349  dprdz  18350  dprdf1o  18352  dprdsn  18356  dprd2da  18362  ablfac1b  18390  pgpfac1lem5  18399  srgbinomlem2  18462  srgbinom  18466  ringi  18481  prdsringd  18533  imasring  18540  opprring  18552  mulgass3  18558  dvrass  18611  kerf1hrm  18664  subrgunit  18719  issubrg2  18721  abvdiv  18758  islss3  18878  prdslmodd  18888  islmhm2  18957  lspsolv  19062  islbs2  19073  islbs3  19074  lbsextlem4  19080  sralmod  19106  issubassa  19243  sraassa  19244  psrbaglecl  19288  psrbagcon  19290  psrgrp  19317  psrlmod  19320  psrring  19330  psrassa  19333  ipdir  19903  ipdi  19904  ipsubdir  19906  ipsubdi  19907  ipass  19909  ipassr  19910  ipassr2  19911  ocvlss  19935  mamudm  20113  matring  20168  matassa  20169  ofco2  20176  mdetunilem1  20337  mdetunilem9  20345  mdetuni0  20346  mdetmul  20348  gsummatr01lem3  20382  iinopn  20632  subbascn  20968  nrmsep2  21070  isnrm3  21073  regsep2  21090  dnsconst  21092  dfconn2  21132  1stcelcls  21174  nllyidm  21202  dislly  21210  upxp  21336  fbasne0  21544  filss  21567  infil  21577  fsubbas  21581  filssufilg  21625  tmdcn2  21803  psmettri  22026  isxmet2d  22042  xmettri  22066  xmetres2  22076  bldisj  22113  blss2ps  22118  blss2  22119  xmstri2  22181  mstri2  22182  xmstri  22183  mstri  22184  xmstri3  22185  mstri3  22186  msrtri  22187  comet  22228  stdbdbl  22232  met2ndci  22237  ngprcan  22324  ngplcan  22325  ngpsubcan  22328  nmtri2  22341  nrgdsdi  22379  nrgdsdir  22380  nlmdsdi  22395  nlmdsdir  22396  blcvx  22509  icccmplem2  22534  pi1grplem  22757  pi1cof  22767  clmpm1dir  22811  cvsdiv  22840  cvsdivcl  22841  cphdivcl  22890  cphsubdir  22916  cphsubdi  22917  cphassr  22920  bcthlem5  23033  rrxcph  23088  volfiniun  23222  volcn  23280  itg1val2  23357  dvconst  23586  dvlip  23660  dvfsumlem4  23696  ftc1a  23704  ulmval  24038  ulmdvlem3  24060  ang180  24444  cvxcl  24611  scvxcvx  24612  sgmmul  24826  logexprlim  24850  dchrabl  24879  motgrp  25338  iscgra1  25602  cgrane1  25604  cgrane2  25605  cgrahl1  25608  cgrahl2  25609  cgracgr  25610  cgratr  25615  cgrabtwn  25617  dfcgra2  25621  sacgr  25622  f1otrge  25652  colinearalglem1  25686  colinearalg  25690  axcgrtr  25695  axlowdimlem16  25737  axeuclidlem  25742  axcontlem7  25750  eengtrkg  25765  eengtrkge  25766  nbfusgrlevtxm2  26167  lfgriswlk  26454  upgrwlkdvde  26502  erclwwlkstr  26802  erclwwlksntr  26814  numclwwlk5  27100  friendship  27111  grpodivdiv  27243  grpomuldivass  27244  ablodivdiv4  27257  ablonnncan  27259  ablonnncan1  27261  nvmdi  27352  dipassr  27550  archiabllem2c  29534  dvrdir  29575  dvrcan5  29578  reofld  29625  pstmfval  29721  tpr2rico  29740  qqhval2lem  29807  qqhvq  29813  issiga  29955  measdivcstOLD  30068  measdivcst  30069  carsggect  30161  signsply0  30408  bnj149  30653  bnj1118  30760  bnj1128  30766  erdszelem9  30889  resconn  30936  cvmseu  30966  cvmlift2lem12  31004  elmrsubrn  31125  mclsind  31175  noprefixmo  31573  cgrid2  31752  segconeu  31760  btwncomim  31762  btwnswapid  31766  cgrxfr  31804  btwnxfr  31805  colineardim1  31810  brofs2  31826  brifs2  31827  idinside  31833  endofsegid  31834  btwnconn1lem7  31842  btwnconn1lem11  31846  btwnconn1  31850  segcon2  31854  seglemin  31862  segletr  31863  btwnsegle  31866  colinbtwnle  31867  broutsideof2  31871  broutsideof3  31875  outsidele  31881  fvray  31890  fvline  31893  linerflx1  31898  ellines  31901  ivthALT  31972  poimirlem32  33073  ftc1anc  33125  sdclem1  33171  sstotbnd2  33205  zerdivemp1x  33378  isdrngo2  33389  iscringd  33429  lsmsat  33775  lfladdcl  33838  lflnegcl  33842  lflvscl  33844  lshpkrlem4  33880  lshpkrlem6  33882  ldualgrplem  33912  lduallmodlem  33919  latmassOLD  33996  latm12  33997  latm32  33998  latmrot  33999  latmmdiN  34001  latmmdir  34002  omlfh1N  34025  omlfh3N  34026  cvlexchb1  34097  cvlexch3  34099  cvlexch4N  34100  cvlatexchb1  34101  cvlsupr2  34110  hlatjass  34136  hlatj12  34137  hlatj32  34138  cvratlem  34187  cvrat  34188  atcvrj0  34194  cvrat2  34195  atltcvr  34201  atexchltN  34207  cvrat3  34208  cvrat4  34209  3dimlem3  34227  3dimlem3OLDN  34228  3at  34256  2atneat  34281  llncmp  34288  2at0mat0  34291  2atmat0  34292  lplnnle2at  34307  llncvrlpln  34324  lplncmp  34328  lplnexllnN  34330  2llnjaN  34332  4atlem11  34375  lplncvrlvol  34382  lvolcmp  34383  2atm2atN  34551  elpaddatriN  34569  paddasslem9  34594  paddass  34604  padd12N  34605  paddssw2  34610  paddss  34611  pmodlem2  34613  pmodN  34616  pmapjlln1  34621  atmod1i1  34623  atmod1i2  34625  pexmidlem2N  34737  pexmidlem6N  34741  pl42N  34749  lhpm0atN  34795  lautlt  34857  lautcvr  34858  lautj  34859  lautm  34860  ltrneq2  34914  cdlemc3  34960  cdlemc4  34961  cdlemd1  34965  cdleme1b  34993  cdleme1  34994  cdleme2  34995  cdleme3e  34999  cdlemefr27cl  35171  cdlemefs27cl  35181  cdleme42mN  35255  cdlemftr2  35334  trljco  35508  tgrpgrplem  35517  tendoplass  35551  tendodi1  35552  tendodi2  35553  cdlemk36  35681  erngdvlem3  35758  erngdvlem3-rN  35766  tendospdi1  35789  dvalveclem  35794  dialss  35815  dvhvaddass  35866  dvhopvsca  35871  dvhlveclem  35877  diblss  35939  diclss  35962  dihmeetlem12N  36087  dihmeetlem15N  36090  dihmeetlem16N  36091  dihmeetlem17N  36092  dihmeetlem18N  36093  dihmeetlem19N  36094  dvh4dimN  36216  lpolvN  36255  lclkr  36302  lclkrs  36308  lcfr  36354  irrapxlem6  36871  jm2.26lem3  37048  dgrsub2  37186  mpaadgr  37205  mendring  37243  mendlmod  37244  mendassa  37245  relexpmulg  37483  iunrelexpmin2  37485  relexpxpmin  37490  neicvgel1  37899  fmuldfeq  39219  stoweidlem43  39567  stoweidlem52  39576  stoweidlem53  39577  stoweidlem56  39580  stoweidlem57  39581  issmfle  40261  issmfgt  40272  issmfge  40285  fmtnoprmfac1  40776  fmtnoprmfac2  40778  upgrwlkupwlk  41009  copissgrp  41096  cznrng  41243  funcringcsetcALTV2lem9  41332  funcringcsetclem9ALTV  41355  ply1ass23l  41458  linccl  41491  lincext1  41531  lincext3  41533  lincresunit2  41555
  Copyright terms: Public domain W3C validator