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

Theorem simpr1 1234
Description: Simplification of conjunction. (Contributed by Jeff Hankins, 17-Nov-2009.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
Assertion
Ref Expression
simpr1 ((𝜑 ∧ (𝜓𝜒𝜃)) → 𝜓)

Proof of Theorem simpr1
StepHypRef Expression
1 simpr 479 . 2 ((𝜑𝜓) → 𝜓)
213ad2antr1 1204 1 ((𝜑 ∧ (𝜓𝜒𝜃)) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
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 1074
This theorem is referenced by:  simplr1OLD  1262  simprr1OLD  1274  simpr11  1333  simpr21  1339  simpr31  1345  simp1r1  1354  simp2r1  1360  simp3r1  1366  3anandis  1583  fpr2g  6639  isopolem  6758  fr3nr  7144  suppfnss  7488  suppfnssOLD  7489  frfi  8370  intrnfi  8487  iinfi  8488  eqsup  8527  fisupcl  8540  cnfcomlem  8769  ackbij1lem15  9248  fpwwe2lem5  9648  dedekindle  10393  ico0  12414  elioc2  12429  elico2  12430  elicc2  12431  iccsplit  12498  fseq1p1m1  12607  elfz0ubfz0  12637  hashtpg  13459  swrdsbslen  13648  swrdspsleq  13649  ccatswrd  13656  tanadd  15096  dvds2ln  15216  qredeq  15573  ressress  16140  mreexexlem4d  16509  mreexexd  16510  0catg  16549  2oppccomf  16586  issubc3  16710  fthmon  16788  fuccocl  16825  fucidcl  16826  invfuc  16835  initoeu2lem0  16864  initoeu2lem1  16865  curf2cl  17072  yonedalem4c  17118  yonedalem3  17121  pospo  17174  latjle12  17263  latjlej1  17266  latnlej2  17272  latlem12  17279  latmlem1  17282  latledi  17290  latmlej11  17291  latjass  17296  latj12  17297  latj32  17298  latj13  17299  latj31  17300  latjrot  17301  latjjdi  17304  latjjdir  17305  latdisdlem  17390  prdsmndd  17524  imasmnd2  17528  frmdmnd  17597  grpsubrcan  17697  grpsubadd  17704  grpsubsub  17705  grpaddsubass  17706  grpsubsub4  17709  grpnnncan2  17713  imasgrp2  17731  mulgnndir  17770  mulgnndirOLD  17771  mulgnn0dir  17772  mulgdir  17774  mulgnnass  17777  mulgnnassOLD  17778  mulgnn0ass  17779  mulgass  17780  mulgsubdir  17783  pwsmulg  17788  issubg2  17810  eqgval  17844  qusgrp  17850  galcan  17937  gacan  17938  oppgmnd  17984  symggrp  18020  pmtrprfv  18073  pmtr3ncom  18095  psgnunilem3  18116  cmn32  18411  cmn12  18413  abladdsub  18420  mulgnn0di  18431  mulgdi  18432  mulgsubdi  18435  dprdss  18628  dprdz  18629  dprdf1o  18631  dprdsn  18635  dprd2da  18641  ablfac1b  18669  pgpfac1lem5  18678  srgbinomlem2  18741  srgbinom  18745  ringi  18760  prdsringd  18812  imasring  18819  opprring  18831  mulgass3  18837  dvrass  18890  kerf1hrm  18945  subrgunit  19000  issubrg2  19002  abvdiv  19039  islss3  19161  prdslmodd  19171  islmhm2  19240  lspsolv  19345  islbs2  19356  islbs3  19357  lbsextlem4  19363  sralmod  19389  issubassa  19526  sraassa  19527  psrbaglecl  19571  psrbagcon  19573  psrgrp  19600  psrlmod  19603  psrring  19613  psrassa  19616  ipdir  20186  ipdi  20187  ipsubdir  20189  ipsubdi  20190  ipass  20192  ipassr  20193  ipassr2  20194  ocvlss  20218  mamudm  20396  matring  20451  matassa  20452  ofco2  20459  mdetunilem1  20620  mdetunilem9  20628  mdetuni0  20629  mdetmul  20631  gsummatr01lem3  20665  iinopn  20909  subbascn  21260  nrmsep2  21362  isnrm3  21365  regsep2  21382  dnsconst  21384  dfconn2  21424  1stcelcls  21466  nllyidm  21494  dislly  21502  upxp  21628  fbasne0  21835  filss  21858  infil  21868  fsubbas  21872  filssufilg  21916  tmdcn2  22094  psmettri  22317  isxmet2d  22333  xmettri  22357  xmetres2  22367  bldisj  22404  blss2ps  22409  blss2  22410  xmstri2  22472  mstri2  22473  xmstri  22474  mstri  22475  xmstri3  22476  mstri3  22477  msrtri  22478  comet  22519  stdbdbl  22523  met2ndci  22528  ngprcan  22615  ngplcan  22616  ngpsubcan  22619  nmtri2  22632  nrgdsdi  22670  nrgdsdir  22671  nlmdsdi  22686  nlmdsdir  22687  blcvx  22802  icccmplem2  22827  pi1grplem  23049  pi1cof  23059  clmpm1dir  23103  cvsdiv  23132  cvsdivcl  23133  cphdivcl  23182  cphsubdir  23208  cphsubdi  23209  cphassr  23212  bcthlem5  23325  rrxcph  23380  volfiniun  23515  volcn  23574  itg1val2  23650  dvconst  23879  dvlip  23955  dvfsumlem4  23991  ftc1a  23999  ulmval  24333  ulmdvlem3  24355  ang180  24743  cvxcl  24910  scvxcvx  24911  sgmmul  25125  logexprlim  25149  dchrabl  25178  motgrp  25637  iscgra1  25901  cgrane1  25903  cgrane2  25904  cgrahl1  25907  cgrahl2  25908  cgracgr  25909  cgratr  25914  cgrabtwn  25916  dfcgra2  25920  sacgr  25921  f1otrge  25951  colinearalglem1  25985  colinearalg  25989  axcgrtr  25994  axlowdimlem16  26036  axeuclidlem  26041  axcontlem7  26049  eengtrkg  26064  eengtrkge  26065  nbfusgrlevtxm2  26478  lfgriswlk  26795  upgrwlkdvde  26843  wwlknbp1  26947  erclwwlktr  27145  erclwwlkntr  27202  frgr2wwlkeqm  27485  numclwlk1lem2f  27514  numclwwlk5  27556  friendship  27567  grpodivdiv  27703  grpomuldivass  27704  ablodivdiv4  27717  ablonnncan  27719  ablonnncan1  27721  nvmdi  27812  dipassr  28010  archiabllem2c  30058  dvrdir  30099  dvrcan5  30102  reofld  30149  pstmfval  30248  tpr2rico  30267  qqhval2lem  30334  qqhvq  30340  issiga  30483  measdivcstOLD  30596  measdivcst  30597  carsggect  30689  signsply0  30937  tgoldbachgtd  31049  bnj149  31252  bnj1118  31359  bnj1128  31365  erdszelem9  31488  resconn  31535  cvmseu  31565  cvmlift2lem12  31603  elmrsubrn  31724  mclsind  31774  frrlem4  32089  frrlem11  32098  noprefixmo  32154  nosupbnd1  32166  ssltss1  32209  cgrid2  32416  segconeu  32424  btwncomim  32426  btwnswapid  32430  cgrxfr  32468  btwnxfr  32469  colineardim1  32474  brofs2  32490  brifs2  32491  idinside  32497  endofsegid  32498  btwnconn1lem7  32506  btwnconn1lem11  32510  btwnconn1  32514  segcon2  32518  seglemin  32526  segletr  32527  btwnsegle  32530  colinbtwnle  32531  broutsideof2  32535  broutsideof3  32539  outsidele  32545  fvray  32554  fvline  32557  linerflx1  32562  ellines  32565  ivthALT  32636  poimirlem32  33754  ftc1anc  33806  sdclem1  33852  sstotbnd2  33886  zerdivemp1x  34059  isdrngo2  34070  iscringd  34110  lsmsat  34798  lfladdcl  34861  lflnegcl  34865  lflvscl  34867  lshpkrlem4  34903  lshpkrlem6  34905  ldualgrplem  34935  lduallmodlem  34942  latmassOLD  35019  latm12  35020  latm32  35021  latmrot  35022  latmmdiN  35024  latmmdir  35025  omlfh1N  35048  omlfh3N  35049  cvlexchb1  35120  cvlexch3  35122  cvlexch4N  35123  cvlatexchb1  35124  cvlsupr2  35133  hlatjass  35159  hlatj12  35160  hlatj32  35161  cvratlem  35210  cvrat  35211  atcvrj0  35217  cvrat2  35218  atltcvr  35224  atexchltN  35230  cvrat3  35231  cvrat4  35232  3dimlem3  35250  3dimlem3OLDN  35251  3at  35279  2atneat  35304  llncmp  35311  2at0mat0  35314  2atmat0  35315  lplnnle2at  35330  llncvrlpln  35347  lplncmp  35351  lplnexllnN  35353  2llnjaN  35355  4atlem11  35398  lplncvrlvol  35405  lvolcmp  35406  2atm2atN  35574  elpaddatriN  35592  paddasslem9  35617  paddass  35627  padd12N  35628  paddssw2  35633  paddss  35634  pmodlem2  35636  pmodN  35639  pmapjlln1  35644  atmod1i1  35646  atmod1i2  35648  pexmidlem2N  35760  pexmidlem6N  35764  pl42N  35772  lhpm0atN  35818  lautlt  35880  lautcvr  35881  lautj  35882  lautm  35883  ltrneq2  35937  cdlemc3  35983  cdlemc4  35984  cdlemd1  35988  cdleme1b  36016  cdleme1  36017  cdleme2  36018  cdleme3e  36022  cdlemefr27cl  36193  cdlemefs27cl  36203  cdleme42mN  36277  cdlemftr2  36356  trljco  36530  tgrpgrplem  36539  tendoplass  36573  tendodi1  36574  tendodi2  36575  cdlemk36  36703  erngdvlem3  36780  erngdvlem3-rN  36788  tendospdi1  36811  dvalveclem  36816  dialss  36837  dvhvaddass  36888  dvhopvsca  36893  dvhlveclem  36899  diblss  36961  diclss  36984  dihmeetlem12N  37109  dihmeetlem15N  37112  dihmeetlem16N  37113  dihmeetlem17N  37114  dihmeetlem18N  37115  dihmeetlem19N  37116  dvh4dimN  37238  lpolvN  37277  lclkr  37324  lclkrs  37330  lcfr  37376  irrapxlem6  37893  jm2.26lem3  38070  dgrsub2  38207  mpaadgr  38226  mendring  38264  mendlmod  38265  mendassa  38266  relexpmulg  38504  iunrelexpmin2  38506  relexpxpmin  38511  neicvgel1  38919  fmuldfeq  40318  stoweidlem43  40763  stoweidlem52  40772  stoweidlem53  40773  stoweidlem56  40776  stoweidlem57  40777  issmfle  41460  issmfgt  41471  issmfge  41484  fmtnoprmfac1  41987  fmtnoprmfac2  41989  upgrwlkupwlk  42231  copissgrp  42318  cznrng  42465  funcringcsetcALTV2lem9  42554  funcringcsetclem9ALTV  42577  ply1ass23l  42680  linccl  42713  lincext1  42753  lincext3  42755  lincresunit2  42777
  Copyright terms: Public domain W3C validator