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

Theorem simpr1 1186
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 485 . 2 ((𝜑𝜓) → 𝜓)
213ad2antr1 1180 1 ((𝜑 ∧ (𝜓𝜒𝜃)) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  simpr11  1249  simpr21  1252  simpr31  1255  simp1r1  1261  simp2r1  1267  simp3r1  1273  3anandis  1462  fpr2g  6966  isopolem  7087  fr3nr  7482  suppfnss  7846  frfi  8752  intrnfi  8869  iinfi  8870  eqsup  8909  fisupcl  8922  cnfcomlem  9151  ackbij1lem15  9645  fpwwe2lem5  10045  dedekindle  10793  ico0  12774  elioc2  12789  elico2  12790  elicc2  12791  iccsplit  12861  fseq1p1m1  12971  elfz0ubfz0  13001  hashtpg  13833  swrdsbslen  14016  ccatswrd  14020  wwlktovf1  14311  tanadd  15510  dvds2ln  15632  qredeq  15991  ressress  16552  mreexexlem4d  16908  mreexexd  16909  0catg  16948  2oppccomf  16985  issubc3  17109  fthmon  17187  fuccocl  17224  fucidcl  17225  invfuc  17234  initoeu2lem0  17263  initoeu2lem1  17264  curf2cl  17471  yonedalem4c  17517  yonedalem3  17520  pospo  17573  latjle12  17662  latjlej1  17665  latnlej2  17671  latlem12  17678  latmlem1  17681  latledi  17689  latmlej11  17690  latjass  17695  latj12  17696  latj32  17697  latj13  17698  latj31  17699  latjrot  17700  latjjdi  17703  latjjdir  17704  latdisdlem  17789  prdsmndd  17934  imasmnd2  17938  mndissubm  17962  frmdmnd  18014  grpsubrcan  18120  grpsubadd  18127  grpsubsub  18128  grpaddsubass  18129  grpsubsub4  18132  grpnnncan2  18136  imasgrp2  18154  mulgnndir  18196  mulgnn0dir  18197  mulgdir  18199  mulgnnass  18202  mulgnn0ass  18203  mulgass  18204  mulgsubdir  18207  pwsmulg  18212  issubg2  18234  eqgval  18269  qusgrp  18275  galcan  18374  gacan  18375  oppgmnd  18422  pmtrprfv  18512  pmtr3ncom  18534  psgnunilem3  18555  cmn32  18856  cmn12  18858  abladdsub  18866  mulgnn0di  18877  mulgdi  18878  mulgsubdi  18881  dprdss  19082  dprdz  19083  dprdf1o  19085  dprdsn  19089  dprd2da  19095  ablfac1b  19123  pgpfac1lem5  19132  srgbinomlem2  19222  srgbinom  19226  ringi  19241  prdsringd  19293  imasring  19300  opprring  19312  mulgass3  19318  dvrass  19371  kerf1ghm  19428  kerf1hrmOLD  19429  subrgunit  19484  issubrg2  19486  abvdiv  19539  islss3  19662  prdslmodd  19672  islmhm2  19741  lspsolv  19846  islbs2  19857  islbs3  19858  lbsextlem4  19864  sralmod  19890  sraassa  20029  psrbaglecl  20079  psrbagcon  20081  psrgrp  20108  psrlmod  20111  psrring  20121  psrassa  20124  ipdir  20713  ipdi  20714  ipsubdir  20716  ipsubdi  20717  ipass  20719  ipassr  20720  ipassr2  20721  ocvlss  20746  mamudm  20929  matring  20982  matassa  20983  ofco2  20990  mdetunilem1  21151  mdetunilem9  21159  mdetuni0  21160  mdetmul  21162  gsummatr01lem3  21196  iinopn  21440  subbascn  21792  nrmsep2  21894  isnrm3  21897  regsep2  21914  dnsconst  21916  dfconn2  21957  1stcelcls  21999  nllyidm  22027  dislly  22035  upxp  22161  fbasne0  22368  filss  22391  infil  22401  fsubbas  22405  filssufilg  22449  tmdcn2  22627  psmettri  22850  isxmet2d  22866  xmettri  22890  xmetres2  22900  bldisj  22937  blss2ps  22942  blss2  22943  xmstri2  23005  mstri2  23006  xmstri  23007  mstri  23008  xmstri3  23009  mstri3  23010  msrtri  23011  comet  23052  stdbdbl  23056  met2ndci  23061  ngprcan  23148  ngplcan  23149  ngpsubcan  23152  nmtri2  23165  nrgdsdi  23203  nrgdsdir  23204  nlmdsdi  23219  nlmdsdir  23220  blcvx  23335  icccmplem2  23360  pi1grplem  23582  pi1cof  23592  clmpm1dir  23636  cvsdiv  23665  cvsdivcl  23666  cphdivcl  23715  cphsubdir  23741  cphsubdi  23742  cphassr  23745  bcthlem5  23860  rrxcph  23924  volfiniun  24077  volcn  24136  itg1val2  24214  dvconst  24443  dvlip  24519  dvfsumlem4  24555  ftc1a  24563  ulmval  24897  ulmdvlem3  24919  ang180  25319  cvxcl  25490  scvxcvx  25491  sgmmul  25705  logexprlim  25729  dchrabl  25758  motgrp  26257  iscgra1  26524  cgrane1  26526  cgrane2  26527  cgrahl1  26530  cgrahl2  26531  cgracgr  26532  cgratr  26537  cgrabtwn  26540  dfcgra2  26544  sacgr  26545  f1otrge  26586  colinearalglem1  26620  colinearalg  26624  axcgrtr  26629  axlowdimlem16  26671  axeuclidlem  26676  axcontlem7  26684  eengtrkg  26700  eengtrkge  26701  nbfusgrlevtxm2  27088  lfgriswlk  27398  upgrwlkdvde  27446  wwlknbp1  27550  erclwwlktr  27728  erclwwlkntr  27778  frgr2wwlkeqm  28038  numclwwlk1lem2f  28062  numclwwlk5  28095  friendship  28106  grpodivdiv  28245  grpomuldivass  28246  ablodivdiv4  28259  ablonnncan1  28262  nvmdi  28353  dipassr  28551  archiabllem2c  30752  dvrdir  30789  dvrcan5  30792  reofld  30841  eqgvscpbl  30847  qusscaval  30849  quslmod  30851  quslmhm  30852  drgextlsp  30896  ccfldsrarelvec  30956  pstmfval  31036  tpr2rico  31055  qqhval2lem  31122  qqhvq  31128  issiga  31271  measdivcst  31383  measdivcstALTV  31384  carsggect  31476  signsply0  31721  tgoldbachgtd  31833  bnj149  32047  bnj1118  32154  bnj1128  32160  erdszelem9  32344  resconn  32391  cvmseu  32421  cvmlift2lem12  32459  ex-sategoelel  32566  elmrsubrn  32665  mclsind  32715  frrlem4  33024  frrlem8  33028  noprefixmo  33100  nosupbnd1  33112  ssltss1  33155  cgrid2  33362  segconeu  33370  btwncomim  33372  btwnswapid  33376  cgrxfr  33414  btwnxfr  33415  colineardim1  33420  brofs2  33436  brifs2  33437  idinside  33443  endofsegid  33444  btwnconn1lem7  33452  btwnconn1lem11  33456  btwnconn1  33460  segcon2  33464  seglemin  33472  segletr  33473  btwnsegle  33476  colinbtwnle  33477  broutsideof2  33481  broutsideof3  33485  outsidele  33491  fvray  33500  fvline  33503  linerflx1  33508  ellines  33511  ivthALT  33581  poimirlem32  34806  ftc1anc  34857  sdclem1  34901  sstotbnd2  34935  zerdivemp1x  35108  isdrngo2  35119  iscringd  35159  lsmsat  36026  lfladdcl  36089  lflnegcl  36093  lflvscl  36095  lshpkrlem4  36131  lshpkrlem6  36133  ldualgrplem  36163  lduallmodlem  36170  latmassOLD  36247  latm12  36248  latm32  36249  latmrot  36250  latmmdiN  36252  latmmdir  36253  omlfh1N  36276  omlfh3N  36277  cvlexchb1  36348  cvlexch3  36350  cvlexch4N  36351  cvlatexchb1  36352  cvlsupr2  36361  hlatjass  36388  hlatj12  36389  hlatj32  36390  cvratlem  36439  cvrat  36440  atcvrj0  36446  cvrat2  36447  atltcvr  36453  atexchltN  36459  cvrat3  36460  cvrat4  36461  3dimlem3  36479  3dimlem3OLDN  36480  3at  36508  2atneat  36533  llncmp  36540  2at0mat0  36543  2atmat0  36544  lplnnle2at  36559  llncvrlpln  36576  lplncmp  36580  lplnexllnN  36582  2llnjaN  36584  4atlem11  36627  lplncvrlvol  36634  lvolcmp  36635  2atm2atN  36803  elpaddatriN  36821  paddasslem9  36846  paddass  36856  padd12N  36857  paddssw2  36862  paddss  36863  pmodlem2  36865  pmodN  36868  pmapjlln1  36873  atmod1i1  36875  atmod1i2  36877  pexmidlem2N  36989  pexmidlem6N  36993  pl42N  37001  lhpm0atN  37047  lautlt  37109  lautcvr  37110  lautj  37111  lautm  37112  ltrneq2  37166  cdlemc3  37211  cdlemc4  37212  cdlemd1  37216  cdleme1b  37244  cdleme1  37245  cdleme2  37246  cdleme3e  37250  cdlemefr27cl  37421  cdlemefs27cl  37431  cdleme42mN  37505  cdlemftr2  37584  trljco  37758  tgrpgrplem  37767  tendoplass  37801  tendodi1  37802  tendodi2  37803  cdlemk36  37931  erngdvlem3  38008  erngdvlem3-rN  38016  tendospdi1  38038  dvalveclem  38043  dialss  38064  dvhvaddass  38115  dvhopvsca  38120  dvhlveclem  38126  diblss  38188  diclss  38211  dihmeetlem12N  38336  dihmeetlem15N  38339  dihmeetlem16N  38340  dihmeetlem17N  38341  dihmeetlem18N  38342  dihmeetlem19N  38343  dvh4dimN  38465  lpolvN  38504  lclkr  38551  lclkrs  38557  lcfr  38603  irrapxlem6  39304  jm2.26lem3  39478  dgrsub2  39615  mpaadgr  39634  mendring  39672  mendlmod  39673  mendassa  39674  relexpmulg  39935  iunrelexpmin2  39937  relexpxpmin  39942  neicvgel1  40349  fmuldfeq  41744  stoweidlem43  42209  stoweidlem52  42218  stoweidlem53  42219  stoweidlem56  42222  stoweidlem57  42223  issmfle  42903  issmfgt  42914  issmfge  42927  fmtnoprmfac1  43574  fmtnoprmfac2  43576  upgrwlkupwlk  43862  copissgrp  43922  cznrng  44124  funcringcsetcALTV2lem9  44213  funcringcsetclem9ALTV  44236  ply1ass23l  44334  linccl  44367  lincext1  44407  lincext3  44409  lincresunit2  44431  line  44617  rrxline  44619  itsclc0yqsol  44649
  Copyright terms: Public domain W3C validator