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

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

Proof of Theorem simpr2
StepHypRef Expression
1 simpr 485 . 2 ((𝜑𝜒) → 𝜒)
213ad2antr2 1181 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:  simpr12  1250  simpr22  1253  simpr32  1256  simp1r2  1262  simp2r2  1268  simp3r2  1274  3anandis  1462  fpr2g  6965  isopolem  7087  fr3nr  7483  frfi  8751  intrnfi  8868  fisupcl  8921  cnfcomlem  9150  ackbij1lem15  9644  cofsmo  9679  sornom  9687  fpwwe2lem5  10044  dedekindle  10792  supmul1  11598  eluzuzle  12240  xlesubadd  12644  elioc2  12787  elico2  12788  elicc2  12789  fseq1p1m1  12969  fz0fzelfz0  13001  swrdsbslen  14014  ccatswrd  14018  swrdswrdlem  14054  wwlktovf1  14309  tanadd  15508  dvds2ln  15630  cshwsidrepsw  16415  ressress  16550  f1ovscpbl  16787  mreexexlem4d  16906  mreexexd  16907  iscatd2  16940  2oppccomf  16983  issubc3  17107  fthmon  17185  fuccocl  17222  fucidcl  17223  invfuc  17232  initoeu2lem0  17261  initoeu2lem1  17262  curf2cl  17469  yonedalem4c  17515  yonedalem3  17518  pospo  17571  latjle12  17660  latjlej1  17663  latnlej2  17669  latlem12  17676  latmlem1  17679  latledi  17687  latjass  17693  latj12  17694  latj32  17695  latj13  17696  latj31  17697  latjrot  17698  latjjdi  17701  latjjdir  17702  latdisdlem  17787  prdsmndd  17932  mndissubm  17960  frmdmnd  18012  grpsubrcan  18118  grpsubadd  18125  grpaddsubass  18127  grpsubsub4  18130  grppnpcan2  18131  grpnpncan  18132  mulgnndir  18194  mulgnn0dir  18195  mulgdir  18197  mulgnnass  18200  mulgnn0ass  18201  mulgass  18202  mulgsubdir  18205  pwsmulg  18210  issubg2  18232  eqgval  18267  qusgrp  18273  galcan  18372  gacan  18373  oppgmnd  18420  fvcosymgeq  18486  pmtrprfv  18510  psgnunilem3  18553  cmn32  18854  cmn12  18856  abladdsub  18864  ablsubsub23  18874  mulgdi  18876  mulgsubdi  18879  dprdss  19080  dprdz  19081  dprdf1o  19083  dprdsn  19087  dprd2da  19093  dmdprdsplit  19098  ablfac1b  19121  pgpfac1lem5  19130  srgi  19190  srgbinom  19224  ringi  19239  prdsringd  19291  opprring  19310  mulgass3  19316  dvrass  19369  subrgunit  19482  issubrg2  19484  abvdiv  19537  lsssn0  19648  islss3  19660  prdslmodd  19670  islmhm2  19739  lspsolv  19844  islbs2  19855  islbs3  19856  lbsextlem4  19862  sralmod  19888  sraassa  20027  psrbaglesupp  20076  psrbaglecl  20077  psrbagcon  20079  psrgrp  20106  psrlmod  20109  psrring  20119  psrassa  20122  psgndiflemB  20672  ipdir  20711  ipdi  20712  ipsubdir  20714  ipsubdi  20715  ipass  20717  ipassr  20718  ipassr2  20719  isphld  20726  ocvlss  20744  mamudm  20927  matring  20980  matassa  20981  ofco2  20988  ma1repveval  21108  mdetunilem1  21149  mdetunilem9  21157  chpscmatgsumbin  21380  iinopn  21438  restopnb  21711  subbascn  21790  nrmsep2  21892  isnrm3  21895  regsep2  21912  dnsconst  21914  dfconn2  21955  1stcelcls  21997  dislly  22033  ptuni2  22112  tx1stc  22186  0nelfb  22367  infil  22399  fsubbas  22403  filssufilg  22447  hauspwpwf1  22523  cnextcn  22603  tmdcn2  22625  ustuqtoplem  22775  utopsnneiplem  22783  psmettri  22848  isxmet2d  22864  xmettri  22888  xmetres2  22898  bldisj  22935  blss2ps  22940  blss2  22941  xmstri2  23003  mstri2  23004  xmstri  23005  mstri  23006  xmstri3  23007  mstri3  23008  msrtri  23009  comet  23050  stdbdbl  23054  met2ndci  23059  ngprcan  23146  ngplcan  23147  ngpsubcan  23150  nmtri2  23163  nrgdsdi  23201  nrgdsdir  23202  nlmdsdi  23217  nlmdsdir  23218  blcvx  23333  icoopnst  23470  pi1grplem  23580  clmpm1dir  23634  cmodscmulexp  23653  cvsdiv  23663  cvsdivcl  23664  cphdivcl  23713  cphsubdir  23739  cphsubdi  23740  tcphcph  23767  bcthlem5  23858  volfiniun  24075  volcn  24134  itg1val2  24212  dvconst  24441  dvlip  24517  ftc1a  24561  ulmval  24895  ulmdvlem3  24917  ang180  25319  cvxcl  25489  scvxcvx  25490  sgmmul  25704  dchrabl  25757  gausslemma2dlem1a  25868  motgrp  26256  iscgra1  26523  cgrane1  26525  cgrane3  26527  cgrahl1  26529  cgrahl2  26530  cgracgr  26531  cgratr  26536  cgrabtwn  26539  cgrahl  26540  dfcgra2  26543  sacgr  26544  f1otrge  26585  colinearalglem1  26619  axcgrtr  26628  axeuclidlem  26675  axcontlem3  26679  axcontlem4  26680  axcontlem7  26683  eengtrkg  26699  eengtrkge  26700  edglnl  26855  subgruhgredgd  26993  nbfusgrlevtxm2  27087  lfgriswlk  27397  wwlknbp1  27549  umgrwwlks2on  27663  rusgrnumwwlks  27680  clwlkclwwlkfo  27714  3spthd  27882  3vfriswmgr  27984  frgr2wwlkeqm  28037  numclwwlk1lem2f  28061  numclwwlk2  28087  numclwwlk3  28091  numclwwlk5  28094  grpomuldivass  28245  ablomuldiv  28256  ablodivdiv4  28258  ablonnncan1  28261  nvmdi  28352  dipassr  28550  archiabllem2c  30751  dvrdir  30788  dvrcan5  30791  reofld  30840  eqgvscpbl  30846  qusscaval  30848  quslmod  30850  quslmhm  30851  drgextlsp  30895  ccfldsrarelvec  30955  pstmfval  31035  qqhval2lem  31121  qqhvq  31127  measdivcst  31382  measdivcstALTV  31383  carsggect  31475  tgoldbachgtd  31832  bnj1098  31954  bnj149  32046  bnj1118  32153  erdszelem9  32343  resconn  32390  cvmseu  32420  cvmlift2lem10  32456  cvmlift2lem12  32458  ex-sategoelel  32565  elmrsubrn  32664  mclsind  32714  noprefixmo  33099  nosupbnd1  33111  ssltss2  33155  cgrid2  33361  segconeu  33369  btwncomim  33371  btwnswapid  33375  trisegint  33386  cgrxfr  33413  brofs2  33435  endofsegid  33443  btwnconn2  33460  seglemin  33471  segletr  33472  btwnsegle  33475  colinbtwnle  33476  broutsideof2  33480  btwnoutside  33483  broutsideof3  33484  outsideoftr  33487  outsidele  33490  fvray  33499  fvline  33502  ellines  33510  broucube  34807  ftc1anc  34856  sdclem1  34899  sstotbnd2  34933  iscringd  35157  lsmsat  36024  lfladdcl  36087  lflnegcl  36091  lflvscl  36093  eqlkr  36115  lshpkrlem4  36129  lshpkrlem6  36131  ldualgrplem  36161  lduallmodlem  36168  latmassOLD  36245  latm12  36246  latm32  36247  latmrot  36248  latmmdiN  36250  latmmdir  36251  omlfh1N  36274  omlfh3N  36275  cvrnbtwn2  36291  cvlexchb1  36346  cvlsupr2  36359  hlatjass  36386  hlatj12  36387  hlatj32  36388  cvrat  36438  cvrat2  36445  atltcvr  36451  atexchltN  36457  cvrat3  36458  cvrat4  36459  atbtwnexOLDN  36463  atbtwnex  36464  3dimlem3  36477  3dimlem3OLDN  36478  3at  36506  2atneat  36531  llncmp  36538  2at0mat0  36541  2atmat0  36542  llncvrlpln  36574  lplncmp  36578  2llnjaN  36582  4atlem11  36625  lplncvrlvol  36632  lvolcmp  36633  2atm2atN  36801  elpaddatriN  36819  paddasslem8  36843  paddass  36854  padd12N  36855  paddssw2  36860  paddss  36861  pmod1i  36864  pmodN  36866  pmapjlln1  36871  atmod1i1  36873  atmod1i2  36875  pexmidlem2N  36987  pl42lem2N  36996  pl42lem3N  36997  pl42lem4N  36998  pl42N  36999  lhpm0atN  37045  lautlt  37107  lautcvr  37108  lautj  37109  lautm  37110  ltrneq2  37164  cdlemd1  37214  cdleme1b  37242  cdleme1  37243  cdleme2  37244  cdleme3e  37248  cdlemefr27cl  37419  cdlemefs27cl  37429  cdleme42ke  37501  cdleme42mN  37503  cdlemf2  37578  cdlemftr2  37582  trljco  37756  tgrpgrplem  37765  tendoplass  37799  tendodi1  37800  tendodi2  37801  cdlemk34  37926  cdlemk36  37929  erngdvlem3-rN  38014  tendospdi1  38036  dialss  38062  dvhvaddass  38113  dvhopvsca  38118  dvhlveclem  38124  diblss  38186  diclss  38209  diclspsn  38210  cdlemn11pre  38226  dihmeetlem12N  38334  dihmeetlem16N  38338  dihmeetlem17N  38339  dihmeetlem18N  38340  dvh4dimN  38463  lpolconN  38503  dochpolN  38506  lclkr  38549  lclkrs  38555  lcfr  38601  irrapxlem6  39302  jm2.26lem3  39476  dgrsub2  39613  mpaaroot  39633  mendring  39670  mendlmod  39671  mendassa  39672  relexpmulg  39933  iunrelexpmin2  39935  relexpxpmin  39940  neicvgel1  40347  grumnud  40499  rfcnpre3  41167  fmuldfeq  41740  xlimbr  41984  stoweidlem43  42205  stoweidlem52  42214  stoweidlem53  42215  stoweidlem56  42218  stoweidlem57  42219  stoweidlem60  42222  issmfle  42899  issmfgt  42910  issmfge  42923  smflimlem4  42927  ltsubsubaddltsub  43378  iccpartigtl  43460  iccelpart  43470  prproropf1olem1  43542  fpprel2  43783  upgrwlkupwlk  43892  copissgrp  43952  cznrng  44154  funcringcsetcALTV2lem9  44243  funcringcsetclem9ALTV  44266  ldepsprlem  44455  lincresunit3  44464  lincreslvec3  44465  itsclc0yqe  44676  itsclc0yqsol  44679
  Copyright terms: Public domain W3C validator