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

Theorem simpr1 1241
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 473 . 2 ((𝜑𝜓) → 𝜓)
213ad2antr1 1232 1 ((𝜑 ∧ (𝜓𝜒𝜃)) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  simplr1OLD  1269  simprr1OLD  1281  simpr11  1340  simpr21  1346  simpr31  1352  simp1r1  1361  simp2r1  1367  simp3r1  1373  3anandis  1588  fpr2g  6700  isopolem  6819  fr3nr  7209  suppfnss  7554  suppfnssOLD  7555  frfi  8444  intrnfi  8561  iinfi  8562  eqsup  8601  fisupcl  8614  cnfcomlem  8843  ackbij1lem15  9341  fpwwe2lem5  9741  dedekindle  10486  ico0  12439  elioc2  12454  elico2  12455  elicc2  12456  iccsplit  12528  fseq1p1m1  12637  elfz0ubfz0  12667  hashtpg  13484  swrdsbslen  13672  swrdspsleq  13673  ccatswrd  13680  tanadd  15117  dvds2ln  15237  qredeq  15589  ressress  16150  mreexexlem4d  16512  mreexexd  16513  0catg  16552  2oppccomf  16589  issubc3  16713  fthmon  16791  fuccocl  16828  fucidcl  16829  invfuc  16838  initoeu2lem0  16867  initoeu2lem1  16868  curf2cl  17076  yonedalem4c  17122  yonedalem3  17125  pospo  17178  latjle12  17267  latjlej1  17270  latnlej2  17276  latlem12  17283  latmlem1  17286  latledi  17294  latmlej11  17295  latjass  17300  latj12  17301  latj32  17302  latj13  17303  latj31  17304  latjrot  17305  latjjdi  17308  latjjdir  17309  latdisdlem  17394  prdsmndd  17528  imasmnd2  17532  frmdmnd  17601  grpsubrcan  17701  grpsubadd  17708  grpsubsub  17709  grpaddsubass  17710  grpsubsub4  17713  grpnnncan2  17717  imasgrp2  17735  mulgnndir  17773  mulgnn0dir  17774  mulgdir  17776  mulgnnass  17779  mulgnn0ass  17780  mulgass  17781  mulgsubdir  17784  pwsmulg  17789  issubg2  17811  eqgval  17845  qusgrp  17851  galcan  17938  gacan  17939  oppgmnd  17985  symggrp  18021  pmtrprfv  18074  pmtr3ncom  18096  psgnunilem3  18117  cmn32  18412  cmn12  18414  abladdsub  18421  mulgnn0di  18432  mulgdi  18433  mulgsubdi  18436  dprdss  18630  dprdz  18631  dprdf1o  18633  dprdsn  18637  dprd2da  18643  ablfac1b  18671  pgpfac1lem5  18680  srgbinomlem2  18743  srgbinom  18747  ringi  18762  prdsringd  18814  imasring  18821  opprring  18833  mulgass3  18839  dvrass  18892  kerf1hrm  18947  subrgunit  19002  issubrg2  19004  abvdiv  19041  islss3  19166  prdslmodd  19176  islmhm2  19245  lspsolv  19351  islbs2  19363  islbs3  19364  lbsextlem4  19370  sralmod  19396  issubassa  19533  sraassa  19534  psrbaglecl  19578  psrbagcon  19580  psrgrp  19607  psrlmod  19610  psrring  19620  psrassa  19623  ipdir  20194  ipdi  20195  ipsubdir  20197  ipsubdi  20198  ipass  20200  ipassr  20201  ipassr2  20202  ocvlss  20226  mamudm  20404  matring  20459  matassa  20460  ofco2  20468  mdetunilem1  20629  mdetunilem9  20637  mdetuni0  20638  mdetmul  20640  gsummatr01lem3  20675  iinopn  20920  subbascn  21272  nrmsep2  21374  isnrm3  21377  regsep2  21394  dnsconst  21396  dfconn2  21436  1stcelcls  21478  nllyidm  21506  dislly  21514  upxp  21640  fbasne0  21847  filss  21870  infil  21880  fsubbas  21884  filssufilg  21928  tmdcn2  22106  psmettri  22329  isxmet2d  22345  xmettri  22369  xmetres2  22379  bldisj  22416  blss2ps  22421  blss2  22422  xmstri2  22484  mstri2  22485  xmstri  22486  mstri  22487  xmstri3  22488  mstri3  22489  msrtri  22490  comet  22531  stdbdbl  22535  met2ndci  22540  ngprcan  22627  ngplcan  22628  ngpsubcan  22631  nmtri2  22644  nrgdsdi  22682  nrgdsdir  22683  nlmdsdi  22698  nlmdsdir  22699  blcvx  22814  icccmplem2  22839  pi1grplem  23061  pi1cof  23071  clmpm1dir  23115  cvsdiv  23144  cvsdivcl  23145  cphdivcl  23194  cphsubdir  23220  cphsubdi  23221  cphassr  23224  bcthlem5  23337  rrxcph  23392  volfiniun  23528  volcn  23587  itg1val2  23665  dvconst  23894  dvlip  23970  dvfsumlem4  24006  ftc1a  24014  ulmval  24348  ulmdvlem3  24370  ang180  24758  cvxcl  24925  scvxcvx  24926  sgmmul  25140  logexprlim  25164  dchrabl  25193  motgrp  25652  iscgra1  25916  cgrane1  25918  cgrane2  25919  cgrahl1  25922  cgrahl2  25923  cgracgr  25924  cgratr  25929  cgrabtwn  25931  dfcgra2  25935  sacgr  25936  f1otrge  25966  colinearalglem1  26000  colinearalg  26004  axcgrtr  26009  axlowdimlem16  26051  axeuclidlem  26056  axcontlem7  26064  eengtrkg  26079  eengtrkge  26080  nbfusgrlevtxm2  26496  lfgriswlk  26813  upgrwlkdvde  26861  wwlknbp1  26965  erclwwlktr  27165  erclwwlkntr  27222  frgr2wwlkeqm  27506  numclwwlk1lem2f  27534  numclwwlk5  27576  friendship  27587  grpodivdiv  27723  grpomuldivass  27724  ablodivdiv4  27737  ablonnncan1  27740  nvmdi  27831  dipassr  28029  archiabllem2c  30074  dvrdir  30115  dvrcan5  30118  reofld  30165  pstmfval  30264  tpr2rico  30283  qqhval2lem  30350  qqhvq  30356  issiga  30499  measdivcstOLD  30612  measdivcst  30613  carsggect  30705  signsply0  30953  tgoldbachgtd  31065  bnj149  31268  bnj1118  31375  bnj1128  31381  erdszelem9  31504  resconn  31551  cvmseu  31581  cvmlift2lem12  31619  elmrsubrn  31740  mclsind  31790  frrlem4  32104  frrlem11  32113  noprefixmo  32169  nosupbnd1  32181  ssltss1  32224  cgrid2  32431  segconeu  32439  btwncomim  32441  btwnswapid  32445  cgrxfr  32483  btwnxfr  32484  colineardim1  32489  brofs2  32505  brifs2  32506  idinside  32512  endofsegid  32513  btwnconn1lem7  32521  btwnconn1lem11  32525  btwnconn1  32529  segcon2  32533  seglemin  32541  segletr  32542  btwnsegle  32545  colinbtwnle  32546  broutsideof2  32550  broutsideof3  32554  outsidele  32560  fvray  32569  fvline  32572  linerflx1  32577  ellines  32580  ivthALT  32651  poimirlem32  33754  ftc1anc  33805  sdclem1  33850  sstotbnd2  33884  zerdivemp1x  34057  isdrngo2  34068  iscringd  34108  lsmsat  34788  lfladdcl  34851  lflnegcl  34855  lflvscl  34857  lshpkrlem4  34893  lshpkrlem6  34895  ldualgrplem  34925  lduallmodlem  34932  latmassOLD  35009  latm12  35010  latm32  35011  latmrot  35012  latmmdiN  35014  latmmdir  35015  omlfh1N  35038  omlfh3N  35039  cvlexchb1  35110  cvlexch3  35112  cvlexch4N  35113  cvlatexchb1  35114  cvlsupr2  35123  hlatjass  35150  hlatj12  35151  hlatj32  35152  cvratlem  35201  cvrat  35202  atcvrj0  35208  cvrat2  35209  atltcvr  35215  atexchltN  35221  cvrat3  35222  cvrat4  35223  3dimlem3  35241  3dimlem3OLDN  35242  3at  35270  2atneat  35295  llncmp  35302  2at0mat0  35305  2atmat0  35306  lplnnle2at  35321  llncvrlpln  35338  lplncmp  35342  lplnexllnN  35344  2llnjaN  35346  4atlem11  35389  lplncvrlvol  35396  lvolcmp  35397  2atm2atN  35565  elpaddatriN  35583  paddasslem9  35608  paddass  35618  padd12N  35619  paddssw2  35624  paddss  35625  pmodlem2  35627  pmodN  35630  pmapjlln1  35635  atmod1i1  35637  atmod1i2  35639  pexmidlem2N  35751  pexmidlem6N  35755  pl42N  35763  lhpm0atN  35809  lautlt  35871  lautcvr  35872  lautj  35873  lautm  35874  ltrneq2  35928  cdlemc3  35974  cdlemc4  35975  cdlemd1  35979  cdleme1b  36007  cdleme1  36008  cdleme2  36009  cdleme3e  36013  cdlemefr27cl  36184  cdlemefs27cl  36194  cdleme42mN  36268  cdlemftr2  36347  trljco  36521  tgrpgrplem  36530  tendoplass  36564  tendodi1  36565  tendodi2  36566  cdlemk36  36694  erngdvlem3  36771  erngdvlem3-rN  36779  tendospdi1  36801  dvalveclem  36806  dialss  36827  dvhvaddass  36878  dvhopvsca  36883  dvhlveclem  36889  diblss  36951  diclss  36974  dihmeetlem12N  37099  dihmeetlem15N  37102  dihmeetlem16N  37103  dihmeetlem17N  37104  dihmeetlem18N  37105  dihmeetlem19N  37106  dvh4dimN  37228  lpolvN  37267  lclkr  37314  lclkrs  37320  lcfr  37366  irrapxlem6  37893  jm2.26lem3  38069  dgrsub2  38206  mpaadgr  38225  mendring  38263  mendlmod  38264  mendassa  38265  relexpmulg  38502  iunrelexpmin2  38504  relexpxpmin  38509  neicvgel1  38917  fmuldfeq  40295  stoweidlem43  40739  stoweidlem52  40748  stoweidlem53  40749  stoweidlem56  40752  stoweidlem57  40753  issmfle  41436  issmfgt  41447  issmfge  41460  fmtnoprmfac1  42052  fmtnoprmfac2  42054  upgrwlkupwlk  42289  copissgrp  42376  cznrng  42523  funcringcsetcALTV2lem9  42612  funcringcsetclem9ALTV  42635  ply1ass23l  42738  linccl  42771  lincext1  42811  lincext3  42813  lincresunit2  42835
  Copyright terms: Public domain W3C validator