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

Theorem simpr2 1196
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 486 . 2 ((𝜑𝜒) → 𝜒)
213ad2antr2 1190 1 ((𝜑 ∧ (𝜓𝜒𝜃)) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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 206  df-an 398  df-3an 1090
This theorem is referenced by:  simpr12  1259  simpr22  1262  simpr32  1265  simp1r2  1271  simp2r2  1277  simp3r2  1283  3anandis  1472  fpr2g  7162  isopolem  7291  fr3nr  7707  sexp3  8086  dif1en  9105  frfi  9233  intrnfi  9353  fisupcl  9406  cnfcomlem  9636  ackbij1lem15  10171  cofsmo  10206  sornom  10214  fpwwe2lem4  10571  dedekindle  11320  supmul1  12125  eluzuzle  12773  xlesubadd  13183  elioc2  13328  elico2  13329  elicc2  13330  fseq1p1m1  13516  fz0fzelfz0  13548  swrdsbslen  14553  ccatswrd  14557  swrdswrdlem  14593  wwlktovf1  14847  tanadd  16050  dvds2ln  16172  cshwsidrepsw  16967  ressress  17130  f1ovscpbl  17409  mreexexlem4d  17528  mreexexd  17529  iscatd2  17562  2oppccomf  17608  issubc3  17736  fthmon  17815  fuccocl  17854  fucidcl  17855  invfuc  17864  initoeu2lem0  17900  initoeu2lem1  17901  curf2cl  18121  yonedalem4c  18167  yonedalem3  18170  pospo  18235  latjle12  18340  latjlej1  18343  latnlej2  18349  latlem12  18356  latmlem1  18359  latledi  18367  latjass  18373  latj12  18374  latj32  18375  latj13  18376  latj31  18377  latjrot  18378  latjjdi  18381  latjjdir  18382  latdisdlem  18386  prdsmndd  18590  mndissubm  18619  frmdmnd  18670  grpsubrcan  18829  grpsubadd  18836  grpaddsubass  18838  grpsubsub4  18841  grppnpcan2  18842  grpnpncan  18843  mulgnndir  18906  mulgnn0dir  18907  mulgdir  18909  mulgnnass  18912  mulgnn0ass  18913  mulgass  18914  mulgsubdir  18917  pwsmulg  18922  issubg2  18944  eqgval  18980  qusgrp  18986  galcan  19085  gacan  19086  oppgmnd  19136  fvcosymgeq  19212  pmtrprfv  19236  psgnunilem3  19279  cmn32  19583  cmn12  19585  abladdsub  19594  ablsubsub23  19604  mulgdi  19606  mulgsubdi  19609  dprdss  19809  dprdz  19810  dprdf1o  19812  dprdsn  19816  dprd2da  19822  dmdprdsplit  19827  ablfac1b  19850  pgpfac1lem5  19859  srgdilem  19924  srgbinom  19963  ringdilem  19981  prdsringd  20037  opprring  20061  mulgass3  20067  dvrass  20120  subrgunit  20243  issubrg2  20245  abvdiv  20299  lsssn0  20411  islss3  20423  prdslmodd  20433  islmhm2  20502  lspsolv  20607  islbs2  20618  islbs3  20619  lbsextlem4  20625  sralmod  20659  psgndiflemB  21007  ipdir  21046  ipdi  21047  ipsubdir  21049  ipsubdi  21050  ipass  21052  ipassr  21053  ipassr2  21054  isphld  21061  ocvlss  21079  sraassa  21276  psrbaglesuppOLD  21330  psrbagleclOLD  21332  psrbagconOLD  21336  psrgrpOLD  21370  psrlmod  21373  psrring  21383  psrassa  21386  mamudm  21740  matring  21795  matassa  21796  ofco2  21803  ma1repveval  21923  mdetunilem1  21964  mdetunilem9  21972  chpscmatgsumbin  22196  iinopn  22254  restopnb  22529  subbascn  22608  nrmsep2  22710  isnrm3  22713  regsep2  22730  dnsconst  22732  dfconn2  22773  1stcelcls  22815  dislly  22851  ptuni2  22930  tx1stc  23004  0nelfb  23185  infil  23217  fsubbas  23221  filssufilg  23265  hauspwpwf1  23341  cnextcn  23421  tmdcn2  23443  ustuqtoplem  23594  utopsnneiplem  23602  psmettri  23667  isxmet2d  23683  xmettri  23707  xmetres2  23717  bldisj  23754  blss2ps  23759  blss2  23760  xmstri2  23822  mstri2  23823  xmstri  23824  mstri  23825  xmstri3  23826  mstri3  23827  msrtri  23828  comet  23872  stdbdbl  23876  met2ndci  23881  ngprcan  23969  ngplcan  23970  ngpsubcan  23973  nmtri2  23986  nrgdsdi  24032  nrgdsdir  24033  nlmdsdi  24048  nlmdsdir  24049  blcvx  24164  icoopnst  24305  pi1grplem  24415  clmpm1dir  24469  cmodscmulexp  24488  cvsdiv  24498  cvsdivcl  24499  cphdivcl  24549  cphsubdir  24575  cphsubdi  24576  tcphcph  24604  bcthlem5  24695  volfiniun  24914  volcn  24973  itg1val2  25051  dvconst  25284  dvlip  25360  ftc1a  25404  ulmval  25742  ulmdvlem3  25764  ang180  26167  cvxcl  26337  scvxcvx  26338  sgmmul  26552  dchrabl  26605  gausslemma2dlem1a  26716  nosupbnd1  27065  noinfbnd1lem5  27078  noinfbnd1  27080  ssltss2  27132  addscom  27281  motgrp  27488  iscgra1  27755  cgrane1  27757  cgrane3  27759  cgrahl1  27761  cgrahl2  27762  cgracgr  27763  cgratr  27768  cgrabtwn  27771  cgrahl  27772  dfcgra2  27775  sacgr  27776  f1otrge  27817  colinearalglem1  27858  axcgrtr  27867  axeuclidlem  27914  axcontlem3  27918  axcontlem4  27919  axcontlem7  27922  eengtrkg  27938  eengtrkge  27939  edglnl  28097  subgruhgredgd  28235  nbfusgrlevtxm2  28329  lfgriswlk  28639  wwlknbp1  28792  umgrwwlks2on  28905  rusgrnumwwlks  28922  clwlkclwwlkfo  28956  3spthd  29123  3vfriswmgr  29225  frgr2wwlkeqm  29278  numclwwlk1lem2f  29302  numclwwlk2  29328  numclwwlk3  29332  numclwwlk5  29335  grpomuldivass  29486  ablomuldiv  29497  ablodivdiv4  29499  ablonnncan1  29502  nvmdi  29593  dipassr  29791  archiabllem2c  32034  dvrdir  32073  dvrcan5  32076  reofld  32139  eqgvscpbl  32145  qusscaval  32147  quslmod  32149  quslmhm  32150  prmidlc  32224  ssmxidl  32242  drgextlsp  32298  ccfldsrarelvec  32358  pstmfval  32480  qqhval2lem  32565  qqhvq  32571  measdivcst  32826  measdivcstALTV  32827  carsggect  32921  tgoldbachgtd  33278  bnj1098  33398  bnj149  33490  bnj1118  33599  erdszelem9  33796  resconn  33843  cvmseu  33873  cvmlift2lem10  33909  cvmlift2lem12  33911  ex-sategoelel  34018  elmrsubrn  34117  mclsind  34167  cgrid2  34591  segconeu  34599  btwncomim  34601  btwnswapid  34605  trisegint  34616  cgrxfr  34643  brofs2  34665  endofsegid  34673  btwnconn2  34690  seglemin  34701  segletr  34702  btwnsegle  34705  colinbtwnle  34706  broutsideof2  34710  btwnoutside  34713  broutsideof3  34714  outsideoftr  34717  outsidele  34720  fvray  34729  fvline  34732  ellines  34740  broucube  36115  ftc1anc  36162  sdclem1  36205  sstotbnd2  36236  iscringd  36460  lsmsat  37473  lfladdcl  37536  lflnegcl  37540  lflvscl  37542  eqlkr  37564  lshpkrlem4  37578  lshpkrlem6  37580  ldualgrplem  37610  lduallmodlem  37617  latmassOLD  37694  latm12  37695  latm32  37696  latmrot  37697  latmmdiN  37699  latmmdir  37700  omlfh1N  37723  omlfh3N  37724  cvrnbtwn2  37740  cvlexchb1  37795  cvlsupr2  37808  hlatjass  37835  hlatj12  37836  hlatj32  37837  cvrat  37888  cvrat2  37895  atltcvr  37901  atexchltN  37907  cvrat3  37908  cvrat4  37909  atbtwnexOLDN  37913  atbtwnex  37914  3dimlem3  37927  3dimlem3OLDN  37928  3at  37956  2atneat  37981  llncmp  37988  2at0mat0  37991  2atmat0  37992  llncvrlpln  38024  lplncmp  38028  2llnjaN  38032  4atlem11  38075  lplncvrlvol  38082  lvolcmp  38083  2atm2atN  38251  elpaddatriN  38269  paddasslem8  38293  paddass  38304  padd12N  38305  paddssw2  38310  paddss  38311  pmod1i  38314  pmodN  38316  pmapjlln1  38321  atmod1i1  38323  atmod1i2  38325  pexmidlem2N  38437  pl42lem2N  38446  pl42lem3N  38447  pl42lem4N  38448  pl42N  38449  lhpm0atN  38495  lautlt  38557  lautcvr  38558  lautj  38559  lautm  38560  ltrneq2  38614  cdlemd1  38664  cdleme1b  38692  cdleme1  38693  cdleme2  38694  cdleme3e  38698  cdlemefr27cl  38869  cdlemefs27cl  38879  cdleme42ke  38951  cdleme42mN  38953  cdlemf2  39028  cdlemftr2  39032  trljco  39206  tgrpgrplem  39215  tendoplass  39249  tendodi1  39250  tendodi2  39251  cdlemk34  39376  cdlemk36  39379  erngdvlem3-rN  39464  tendospdi1  39486  dialss  39512  dvhvaddass  39563  dvhopvsca  39568  dvhlveclem  39574  diblss  39636  diclss  39659  diclspsn  39660  cdlemn11pre  39676  dihmeetlem12N  39784  dihmeetlem16N  39788  dihmeetlem17N  39789  dihmeetlem18N  39790  dvh4dimN  39913  lpolconN  39953  dochpolN  39956  lclkr  39999  lclkrs  40005  lcfr  40051  isdomn4  40627  irrapxlem6  41153  jm2.26lem3  41328  dgrsub2  41465  mpaaroot  41485  mendring  41522  mendlmod  41523  mendassa  41524  relexpmulg  41989  iunrelexpmin2  41991  relexpxpmin  41996  neicvgel1  42398  grumnud  42573  rfcnpre3  43245  fmuldfeq  43831  xlimbr  44075  stoweidlem43  44291  stoweidlem52  44300  stoweidlem53  44301  stoweidlem56  44304  stoweidlem57  44305  stoweidlem60  44308  issmfle  44993  issmfgt  45004  issmfge  45018  smflimlem4  45022  ltsubsubaddltsub  45540  iccpartigtl  45622  iccelpart  45632  prproropf1olem1  45702  fpprel2  45940  upgrwlkupwlk  46049  copissgrp  46109  cznrng  46260  funcringcsetcALTV2lem9  46349  funcringcsetclem9ALTV  46372  ldepsprlem  46560  lincresunit3  46569  lincreslvec3  46570  itsclc0yqe  46854  itsclc0yqsol  46857  topdlat  47036  catprs  47038  endmndlem  47042  idmon  47043  idepi  47044  thincmon  47061  thincepi  47062  functhinclem1  47068  grptcmon  47123  grptcepi  47124
  Copyright terms: Public domain W3C validator