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

Theorem simpr2 1191
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 487 . 2 ((𝜑𝜒) → 𝜒)
213ad2antr2 1185 1 ((𝜑 ∧ (𝜓𝜒𝜃)) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398  w3a 1083
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 209  df-an 399  df-3an 1085
This theorem is referenced by:  simpr12  1254  simpr22  1257  simpr32  1260  simp1r2  1266  simp2r2  1272  simp3r2  1278  3anandis  1467  fpr2g  6950  isopolem  7075  fr3nr  7472  frfi  8741  intrnfi  8858  fisupcl  8911  cnfcomlem  9140  ackbij1lem15  9634  cofsmo  9669  sornom  9677  fpwwe2lem5  10034  dedekindle  10782  supmul1  11588  eluzuzle  12231  xlesubadd  12635  elioc2  12779  elico2  12780  elicc2  12781  fseq1p1m1  12965  fz0fzelfz0  12997  swrdsbslen  14006  ccatswrd  14010  swrdswrdlem  14046  wwlktovf1  14301  tanadd  15500  dvds2ln  15622  cshwsidrepsw  16406  ressress  16541  f1ovscpbl  16778  mreexexlem4d  16897  mreexexd  16898  iscatd2  16931  2oppccomf  16974  issubc3  17098  fthmon  17176  fuccocl  17213  fucidcl  17214  invfuc  17223  initoeu2lem0  17252  initoeu2lem1  17253  curf2cl  17460  yonedalem4c  17506  yonedalem3  17509  pospo  17562  latjle12  17651  latjlej1  17654  latnlej2  17660  latlem12  17667  latmlem1  17670  latledi  17678  latjass  17684  latj12  17685  latj32  17686  latj13  17687  latj31  17688  latjrot  17689  latjjdi  17692  latjjdir  17693  latdisdlem  17778  prdsmndd  17923  mndissubm  17951  frmdmnd  18003  grpsubrcan  18159  grpsubadd  18166  grpaddsubass  18168  grpsubsub4  18171  grppnpcan2  18172  grpnpncan  18173  mulgnndir  18235  mulgnn0dir  18236  mulgdir  18238  mulgnnass  18241  mulgnn0ass  18242  mulgass  18243  mulgsubdir  18246  pwsmulg  18251  issubg2  18273  eqgval  18308  qusgrp  18314  galcan  18413  gacan  18414  oppgmnd  18461  fvcosymgeq  18536  pmtrprfv  18560  psgnunilem3  18603  cmn32  18904  cmn12  18906  abladdsub  18914  ablsubsub23  18924  mulgdi  18926  mulgsubdi  18929  dprdss  19130  dprdz  19131  dprdf1o  19133  dprdsn  19137  dprd2da  19143  dmdprdsplit  19148  ablfac1b  19171  pgpfac1lem5  19180  srgi  19240  srgbinom  19274  ringi  19289  prdsringd  19341  opprring  19360  mulgass3  19366  dvrass  19419  subrgunit  19529  issubrg2  19531  abvdiv  19584  lsssn0  19695  islss3  19707  prdslmodd  19717  islmhm2  19786  lspsolv  19891  islbs2  19902  islbs3  19903  lbsextlem4  19909  sralmod  19935  sraassa  20075  psrbaglesupp  20124  psrbaglecl  20125  psrbagcon  20127  psrgrp  20154  psrlmod  20157  psrring  20167  psrassa  20170  psgndiflemB  20720  ipdir  20759  ipdi  20760  ipsubdir  20762  ipsubdi  20763  ipass  20765  ipassr  20766  ipassr2  20767  isphld  20774  ocvlss  20792  mamudm  20975  matring  21028  matassa  21029  ofco2  21036  ma1repveval  21156  mdetunilem1  21197  mdetunilem9  21205  chpscmatgsumbin  21428  iinopn  21486  restopnb  21759  subbascn  21838  nrmsep2  21940  isnrm3  21943  regsep2  21960  dnsconst  21962  dfconn2  22003  1stcelcls  22045  dislly  22081  ptuni2  22160  tx1stc  22234  0nelfb  22415  infil  22447  fsubbas  22451  filssufilg  22495  hauspwpwf1  22571  cnextcn  22651  tmdcn2  22673  ustuqtoplem  22824  utopsnneiplem  22832  psmettri  22897  isxmet2d  22913  xmettri  22937  xmetres2  22947  bldisj  22984  blss2ps  22989  blss2  22990  xmstri2  23052  mstri2  23053  xmstri  23054  mstri  23055  xmstri3  23056  mstri3  23057  msrtri  23058  comet  23099  stdbdbl  23103  met2ndci  23108  ngprcan  23195  ngplcan  23196  ngpsubcan  23199  nmtri2  23212  nrgdsdi  23250  nrgdsdir  23251  nlmdsdi  23266  nlmdsdir  23267  blcvx  23382  icoopnst  23523  pi1grplem  23633  clmpm1dir  23687  cmodscmulexp  23706  cvsdiv  23716  cvsdivcl  23717  cphdivcl  23766  cphsubdir  23792  cphsubdi  23793  tcphcph  23820  bcthlem5  23911  volfiniun  24130  volcn  24189  itg1val2  24267  dvconst  24499  dvlip  24575  ftc1a  24619  ulmval  24954  ulmdvlem3  24976  ang180  25379  cvxcl  25549  scvxcvx  25550  sgmmul  25764  dchrabl  25817  gausslemma2dlem1a  25928  motgrp  26316  iscgra1  26583  cgrane1  26585  cgrane3  26587  cgrahl1  26589  cgrahl2  26590  cgracgr  26591  cgratr  26596  cgrabtwn  26599  cgrahl  26600  dfcgra2  26603  sacgr  26604  f1otrge  26645  colinearalglem1  26679  axcgrtr  26688  axeuclidlem  26735  axcontlem3  26739  axcontlem4  26740  axcontlem7  26743  eengtrkg  26759  eengtrkge  26760  edglnl  26915  subgruhgredgd  27053  nbfusgrlevtxm2  27147  lfgriswlk  27457  wwlknbp1  27609  umgrwwlks2on  27722  rusgrnumwwlks  27739  clwlkclwwlkfo  27773  3spthd  27940  3vfriswmgr  28042  frgr2wwlkeqm  28095  numclwwlk1lem2f  28119  numclwwlk2  28145  numclwwlk3  28149  numclwwlk5  28152  grpomuldivass  28303  ablomuldiv  28314  ablodivdiv4  28316  ablonnncan1  28319  nvmdi  28410  dipassr  28608  archiabllem2c  30832  dvrdir  30869  dvrcan5  30872  reofld  30921  eqgvscpbl  30927  qusscaval  30929  quslmod  30931  quslmhm  30932  prmidlc  30975  ssmxidl  30990  drgextlsp  31007  ccfldsrarelvec  31067  pstmfval  31147  qqhval2lem  31230  qqhvq  31236  measdivcst  31491  measdivcstALTV  31492  carsggect  31584  tgoldbachgtd  31941  bnj1098  32063  bnj149  32155  bnj1118  32264  erdszelem9  32454  resconn  32501  cvmseu  32531  cvmlift2lem10  32567  cvmlift2lem12  32569  ex-sategoelel  32676  elmrsubrn  32775  mclsind  32825  noprefixmo  33210  nosupbnd1  33222  ssltss2  33266  cgrid2  33472  segconeu  33480  btwncomim  33482  btwnswapid  33486  trisegint  33497  cgrxfr  33524  brofs2  33546  endofsegid  33554  btwnconn2  33571  seglemin  33582  segletr  33583  btwnsegle  33586  colinbtwnle  33587  broutsideof2  33591  btwnoutside  33594  broutsideof3  33595  outsideoftr  33598  outsidele  33601  fvray  33610  fvline  33613  ellines  33621  broucube  34967  ftc1anc  35014  sdclem1  35057  sstotbnd2  35088  iscringd  35312  lsmsat  36180  lfladdcl  36243  lflnegcl  36247  lflvscl  36249  eqlkr  36271  lshpkrlem4  36285  lshpkrlem6  36287  ldualgrplem  36317  lduallmodlem  36324  latmassOLD  36401  latm12  36402  latm32  36403  latmrot  36404  latmmdiN  36406  latmmdir  36407  omlfh1N  36430  omlfh3N  36431  cvrnbtwn2  36447  cvlexchb1  36502  cvlsupr2  36515  hlatjass  36542  hlatj12  36543  hlatj32  36544  cvrat  36594  cvrat2  36601  atltcvr  36607  atexchltN  36613  cvrat3  36614  cvrat4  36615  atbtwnexOLDN  36619  atbtwnex  36620  3dimlem3  36633  3dimlem3OLDN  36634  3at  36662  2atneat  36687  llncmp  36694  2at0mat0  36697  2atmat0  36698  llncvrlpln  36730  lplncmp  36734  2llnjaN  36738  4atlem11  36781  lplncvrlvol  36788  lvolcmp  36789  2atm2atN  36957  elpaddatriN  36975  paddasslem8  36999  paddass  37010  padd12N  37011  paddssw2  37016  paddss  37017  pmod1i  37020  pmodN  37022  pmapjlln1  37027  atmod1i1  37029  atmod1i2  37031  pexmidlem2N  37143  pl42lem2N  37152  pl42lem3N  37153  pl42lem4N  37154  pl42N  37155  lhpm0atN  37201  lautlt  37263  lautcvr  37264  lautj  37265  lautm  37266  ltrneq2  37320  cdlemd1  37370  cdleme1b  37398  cdleme1  37399  cdleme2  37400  cdleme3e  37404  cdlemefr27cl  37575  cdlemefs27cl  37585  cdleme42ke  37657  cdleme42mN  37659  cdlemf2  37734  cdlemftr2  37738  trljco  37912  tgrpgrplem  37921  tendoplass  37955  tendodi1  37956  tendodi2  37957  cdlemk34  38082  cdlemk36  38085  erngdvlem3-rN  38170  tendospdi1  38192  dialss  38218  dvhvaddass  38269  dvhopvsca  38274  dvhlveclem  38280  diblss  38342  diclss  38365  diclspsn  38366  cdlemn11pre  38382  dihmeetlem12N  38490  dihmeetlem16N  38494  dihmeetlem17N  38495  dihmeetlem18N  38496  dvh4dimN  38619  lpolconN  38659  dochpolN  38662  lclkr  38705  lclkrs  38711  lcfr  38757  irrapxlem6  39561  jm2.26lem3  39735  dgrsub2  39872  mpaaroot  39892  mendring  39929  mendlmod  39930  mendassa  39931  relexpmulg  40190  iunrelexpmin2  40192  relexpxpmin  40197  neicvgel1  40604  grumnud  40777  rfcnpre3  41445  fmuldfeq  42016  xlimbr  42260  stoweidlem43  42476  stoweidlem52  42485  stoweidlem53  42486  stoweidlem56  42489  stoweidlem57  42490  stoweidlem60  42493  issmfle  43170  issmfgt  43181  issmfge  43194  smflimlem4  43198  ltsubsubaddltsub  43649  iccpartigtl  43731  iccelpart  43741  prproropf1olem1  43811  fpprel2  44051  upgrwlkupwlk  44160  copissgrp  44220  cznrng  44371  funcringcsetcALTV2lem9  44460  funcringcsetclem9ALTV  44483  ldepsprlem  44672  lincresunit3  44681  lincreslvec3  44682  itsclc0yqe  44935  itsclc0yqsol  44938
  Copyright terms: Public domain W3C validator