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

Theorem simpr3 1089
Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
Assertion
Ref Expression
simpr3 ((𝜑 ∧ (𝜓𝜒𝜃)) → 𝜃)

Proof of Theorem simpr3
StepHypRef Expression
1 simp3 1083 . 2 ((𝜓𝜒𝜃) → 𝜃)
21adantl 481 1 ((𝜑 ∧ (𝜓𝜒𝜃)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054
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 197  df-an 385  df-3an 1056
This theorem is referenced by:  simplr3  1125  simprr3  1131  simp1r3  1179  simp2r3  1185  simp3r3  1191  3anandis  1474  funopsn  6453  fpr2g  6516  isopolem  6635  fr3nr  7021  suppfnss  7365  elfir  8362  intrnfi  8363  fisupcl  8416  cnfcomlem  8634  ackbij1lem15  9094  pwfseqlem4a  9521  pwfseqlem4  9522  eluzuzle  11734  xlesubadd  12131  elioc2  12274  elico2  12275  elicc2  12276  fseq1p1m1  12452  ccatswrd  13502  tanadd  14941  dvds2ln  15061  prmgaplem5  15806  prmgaplem8  15809  cshwsidrepsw  15847  ressress  15985  f1ovscpbl  16233  mreexexlem4d  16354  mreexexd  16355  mreexexdOLD  16356  2oppccomf  16432  fthmon  16634  fuccocl  16671  fucidcl  16672  invfuc  16681  initoeu2lem1  16711  curf2cl  16918  yonedalem4c  16964  yonedalem3  16967  pospo  17020  latjle12  17109  latjlej1  17112  latnlej2  17118  latlem12  17125  latmlem1  17128  latledi  17136  latjass  17142  latj12  17143  latj32  17144  latj13  17145  latj31  17146  latjrot  17147  latjjdi  17150  latjjdir  17151  latdisdlem  17236  prdsmndd  17370  imasmnd2  17374  imasmnd  17375  frmdmnd  17443  grpsubadd  17550  grpaddsubass  17552  grpsubsub4  17555  grppnpcan2  17556  grpnpncan  17557  grpnnncan2  17559  imasgrp2  17577  imasgrp  17578  mulgnndir  17616  mulgnndirOLD  17617  mulgnn0dir  17618  mulgnnass  17623  mulgnnassOLD  17624  mulgnn0ass  17625  mulgass  17626  pwsmulg  17634  issubg2  17656  qusgrp  17696  galcan  17783  gacan  17784  oppgmnd  17830  symggrp  17866  pmtrprfv  17919  pmtr3ncom  17941  psgnunilem3  17962  frgp0  18219  cmn32  18257  cmn12  18259  abladdsub  18266  ablsubsub23  18276  mulgdi  18278  mulgsubdi  18281  dprdss  18474  dprdf1o  18477  dprdsn  18481  dmdprdsplit  18492  pgpfac1lem5  18524  srgi  18557  ringi  18606  prdsringd  18658  imasring  18665  opprring  18677  mulgass3  18683  dvrass  18736  kerf1hrm  18791  subrgunit  18846  issubrg2  18848  abvdiv  18885  lss1  18987  lsssn0  18996  islss3  19007  prdslmodd  19017  islmhm2  19086  lspsolv  19191  lbsextlem4  19209  sralmod  19235  issubassa  19372  sraassa  19373  psrbaglesupp  19416  psrbagcon  19419  psrgrp  19446  psrlmod  19449  psrring  19459  psrassa  19462  mpllsslem  19483  ipdi  20033  ipsubdir  20035  ipsubdi  20036  ipassr  20039  ipassr2  20040  isphld  20047  ocvlss  20064  mamudm  20242  matring  20297  matassa  20298  ofco2  20305  scmatlss  20379  ma1repveval  20425  mdetunilem1  20466  mdetunilem9  20474  monmatcollpw  20632  iinopn  20755  restopnb  21027  subbascn  21106  nrmsep2  21208  isnrm3  21211  t1sep  21222  regsep2  21228  dnsconst  21230  dfconn2  21270  dislly  21348  tx1stc  21501  qtophmeo  21668  filss  21704  infil  21714  fsubbas  21718  filssufilg  21762  hauspwpwf1  21838  cnextcn  21918  tmdcn2  21940  psmettri  22163  isxmet2d  22179  xmettri  22203  xmetres2  22213  bldisj  22250  blss2ps  22255  blss2  22256  xmstri2  22318  mstri2  22319  xmstri  22320  mstri  22321  xmstri3  22322  mstri3  22323  msrtri  22324  comet  22365  met2ndci  22374  ngprcan  22461  ngplcan  22462  ngpsubcan  22465  nmtri2  22478  nrgdsdi  22516  nrgdsdir  22517  nlmdsdi  22532  nlmdsdir  22533  blcvx  22648  iocopnst  22786  icccvx  22796  pi1grplem  22895  pi1xfrf  22899  pi1cof  22905  clmpm1dir  22949  cmodscmulexp  22968  cvsdiv  22978  cvsdivcl  22979  cphdivcl  23028  cphsubdir  23054  cphsubdi  23055  bcthlem5  23171  rrxcph  23226  volfiniun  23361  volcn  23420  itg1val2  23496  dvconst  23725  dvlip  23801  ftc1a  23845  ulmdvlem3  24201  ang180  24589  cvxcl  24756  scvxcvx  24757  sgmmul  24971  logexprlim  24995  dchrabl  25024  motgrp  25483  iscgra1  25747  cgrane2  25750  cgrane4  25752  cgrahl1  25753  cgrahl2  25754  cgracgr  25755  cgratr  25760  cgrabtwn  25762  cgrahl  25763  dfcgra2  25766  sacgr  25767  f1otrge  25797  xmstrkgc  25811  colinearalglem1  25831  colinearalg  25835  axcgrtr  25840  axlowdimlem16  25882  axeuclidlem  25887  axcontlem4  25892  axcontlem7  25895  axcontlem12  25900  eengtrkg  25910  eengtrkge  25911  edglnl  26083  subgruhgredgd  26221  nbfusgrlevtxm2  26324  upgrwlkdvde  26689  crctcshwlkn0lem5  26762  crctcshwlkn0  26769  umgrwwlks2on  26923  rusgrnumwwlks  26941  rusgrnumwlkg  26944  3spthd  27154  frgr2wwlkeqm  27311  numclwwlk5  27375  friendship  27386  grpomuldivass  27523  ablodivdiv4  27536  ablonnncan  27538  dipdi  27826  dipsubdi  27832  disjdsct  29608  omndmul2  29840  archiabllem2c  29877  dvrdir  29918  dvrcan5  29921  reofld  29968  pstmfval  30067  qqhval2lem  30153  qqhvq  30159  esumcvg  30276  sigaclcu  30308  measdivcstOLD  30415  measdivcst  30416  carsggect  30508  tgoldbachgtd  30868  bnj970  31143  bnj910  31144  erdszelem9  31307  cvmseu  31384  elmrsubrn  31543  frrlem11  31917  noprefixmo  31973  nosupbnd1  31985  ssltsep  32030  cgrid2  32235  btwncomim  32245  btwnswapid  32249  trisegint  32260  cgrxfr  32287  btwnxfr  32288  brofs2  32309  brifs2  32310  endofsegid  32317  btwnconn1lem11  32329  btwnconn2  32334  segcon2  32337  seglemin  32345  segletr  32346  btwnsegle  32349  colinbtwnle  32350  broutsideof2  32354  btwnoutside  32357  broutsideof3  32358  outsideoftr  32361  outsidele  32364  ellines  32384  linethrueu  32388  unbdqndv2  32627  poimirlem28  33567  ftc1anc  33623  sdclem1  33669  sstotbnd2  33703  ismndo1  33802  zerdivemp1x  33876  isdrngo2  33887  iscringd  33927  lsmsat  34613  lfladdcl  34676  lflnegcl  34680  lflvscl  34682  lshpkrlem4  34718  lshpkrlem6  34720  ldualgrplem  34750  lduallmodlem  34757  latmassOLD  34834  latm12  34835  latm32  34836  latmrot  34837  latmmdiN  34839  latmmdir  34840  omlfh1N  34863  omlfh3N  34864  cvrnbtwn2  34880  cvlexchb1  34935  cvlexch3  34937  cvlexch4N  34938  cvlatexchb1  34939  cvlsupr2  34948  hlatjass  34974  hlatj12  34975  hlatj32  34976  cvrat  35026  atcvrj0  35032  cvrat2  35033  atltcvr  35039  atexchltN  35045  cvrat3  35046  cvrat4  35047  atbtwnexOLDN  35051  atbtwnex  35052  3dimlem3  35065  3dimlem3OLDN  35066  3at  35094  2atneat  35119  llncmp  35126  2at0mat0  35129  2atmat0  35130  islpln2a  35152  llncvrlpln  35162  lplncmp  35166  3atnelvolN  35190  4atlem11  35213  lplncvrlvol  35220  lvolcmp  35221  2atm2atN  35389  elpaddatriN  35407  elpadd2at2  35411  paddasslem8  35431  paddasslem17  35440  paddass  35442  padd12N  35443  paddssw1  35447  pmodlem2  35451  pmodN  35454  pmapjlln1  35459  atmod1i2  35463  pexmidlem2N  35575  pexmidlem7N  35580  pl42lem2N  35584  pl42lem3N  35585  pl42lem4N  35586  pl42N  35587  lhp2lt  35605  lhpm0atN  35633  lautlt  35695  lautcvr  35696  lautj  35697  lautm  35698  ltrneq2  35752  cdleme1b  35831  cdleme3b  35834  cdleme3c  35835  cdleme9b  35857  cdlemefs27cl  36018  cdleme42mN  36092  cdlemg4c  36217  trljco  36345  tgrpgrplem  36354  tendoplass  36388  tendodi1  36389  tendodi2  36390  erngplus2  36409  erngplus2-rN  36417  cdlemk36  36518  erngdvlem3  36595  erngdvlem3-rN  36603  dvaplusgv  36615  tendospass  36625  tendospdi1  36626  dvalveclem  36631  dialss  36652  dvhvaddass  36703  dvhopvsca  36708  dvhlveclem  36714  diblss  36776  diclss  36799  diclspsn  36800  cdlemn11pre  36816  dihmeetlem12N  36924  dihmeetlem16N  36928  dihmeetlem17N  36929  dvh4dimN  37053  lpolsatN  37094  lpolpolsatN  37095  dochpolN  37096  lclkr  37139  lclkrs  37145  lcfr  37191  irrapxlem6  37708  jm2.26lem3  37885  mpaamn  38043  mendring  38079  mendlmod  38080  mendassa  38081  neicvgel1  38734  rfcnpre4  39507  fmuldfeq  40133  stoweidlem43  40578  stoweidlem52  40587  stoweidlem53  40588  stoweidlem56  40591  issmfgt  41286  issmfge  41299  iccelpart  41694  pfxccat3a  41754  fmtnoprmfac1  41802  fmtnoprmfac2  41804  copissgrp  42133  ringrng  42204  cznrng  42280  funcringcsetcALTV2lem9  42369  funcringcsetclem9ALTV  42392  linccl  42528  lincsumscmcl  42547  ldepsprlem  42586  lincresunit3lem1  42593
  Copyright terms: Public domain W3C validator