MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simpl3 Unicode version

Theorem simpl3 960
Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
Assertion
Ref Expression
simpl3  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ch )

Proof of Theorem simpl3
StepHypRef Expression
1 simp3 957 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ch )
21adantr 451 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  simpll3  996  simprl3  1002  simp1l3  1050  simp2l3  1056  simp3l3  1062  3anandirs  1284  fcofo  5814  soisores  5840  weniso  5868  knatar  5873  smorndom  6401  nnmord  6646  nnmword  6647  difsnen  6960  mapunen  7046  ac6sfi  7117  fipreima  7177  wemaplem2  7278  en2eqpr  7653  indcardi  7684  acndom  7694  fodomfi2  7703  infmap2  7860  cflim2  7905  coftr  7915  infpssrlem4  7948  fin23lem11  7959  fincssdom  7965  isf32lem9  8003  fin1a2lem9  8050  gchpwdom  8312  gruima  8440  prpssnq  8630  distrlem4pr  8666  addcan  9012  addcan2  9013  ledivmul2OLD  9650  supmul1  9735  uzsupss  10326  xaddass  10585  xleadd1a  10589  xlesubadd  10599  xmulasslem3  10622  xadddilem  10630  xadddi  10631  ixxun  10688  icoshftf1o  10775  modsubdir  11024  ltexp2a  11169  leexp2  11172  ltexp2r  11174  exple1  11177  expnlbnd2  11248  ccatass  11452  ccatopth  11478  limsuplt  11969  limsupgre  11971  addcn2  12083  mulcn2  12085  dvdsmod  12601  gcdass  12740  rplpwr  12751  rppwr  12752  rpmulgcd2  12800  rpexp  12815  rpdvds  12819  prmdiveq  12870  coprimeprodsq  12878  coprimeprodsq2  12879  pythagtriplem3  12887  pcdvdsb  12937  pcgcd1  12945  pcbc  12964  0ram  13083  ramz2  13087  ramub1lem1  13089  mremre  13522  mrieqv2d  13557  lubun  14243  issubmnd  14417  gsumccat  14480  frmdss2  14501  mulgnn0p1  14594  mulgnnsubcl  14595  mulgneg  14601  mulgdirlem  14607  nmzsubg  14674  ghmmulg  14711  odmodnn0  14871  oddvdsnn0  14875  odnncl  14876  odmod  14877  oddvds  14878  odeq  14881  odmulgid  14883  odmulg  14885  odmulgeq  14886  odbezout  14887  odf1o1  14899  odf1o2  14900  odngen  14904  odcau  14931  pgpssslw  14941  fislw  14952  lsmless1x  14971  lsmless2x  14972  lsmsubm  14980  lsmmod  15000  lsmmod2  15001  efgsfo  15064  cntzcmn  15152  odadd1  15156  odadd2  15157  odadd  15158  lsmcomx  15164  prdscmnd  15169  gsumconst  15225  rng1eq0  15395  cntzsubr  15593  isabvd  15601  lspss  15757  0lmhm  15813  reslmhm2  15826  lbspss  15851  lspfixed  15897  lsmcv  15910  lspsnat  15914  issubassa  16080  aspss  16088  coe1subfv  16359  coe1tm  16365  xrsdsreclblem  16433  obselocv  16644  neiint  16857  topssnei  16877  cnrest2  17030  cnprest2  17034  cnt0  17090  cnt1  17094  cnhaus  17098  cncmp  17135  fiuncmp  17147  sscmp  17148  hauscmp  17150  cnconn  17164  uncon  17171  kgen2ss  17266  ptpjopn  17322  ptrescn  17349  qtopss  17422  kqfvima  17437  r0cld  17445  cmphaushmeo  17507  fbssint  17549  fbasrn  17595  filuni  17596  ufilmax  17618  fin1aufil  17643  fmf  17656  fmss  17657  rnelfmlem  17663  rnelfm  17664  fmufil  17670  fmco  17672  flimss2  17683  flimss1  17684  flimrest  17694  cnpflf2  17711  cnpflf  17712  flfcnp  17715  lmflf  17716  supnfcls  17731  fclsss1  17733  fclsss2  17734  cnpfcfi  17751  subgntr  17805  opnsubg  17806  cldsubg  17809  bldisj  17971  blgt0  17972  bl2in  17973  blss2  17975  xbln0  17981  blss  17988  lpbl  18065  blcld  18067  blcls  18068  stdbdmopn  18080  metcnp2  18104  txmetcnp  18109  nmoix  18254  nmoi2  18255  nmoeq0  18261  nmotri  18264  metdsge  18369  metds0  18370  metdseq0  18374  icoopnst  18453  iccpnfhmeo  18459  xrhmeo  18460  nmhmcn  18617  cphsqrcl2  18638  cphsqrcl3  18639  fmcfil  18714  bcthlem5  18766  pjth  18819  ovolunnul  18875  volun  18918  voliunlem2  18924  itg2const  19111  iblconst  19188  itgconst  19189  limcvallem  19237  dvcnp2  19285  dvcn  19286  deg1mul3le  19518  deg1tmle  19519  ig1pdvds  19578  coe11  19650  dgrmulc  19668  dvply1  19680  aaliou2  19736  efcvx  19841  tanord  19916  logdivlti  19987  logccv  20026  recxpcl  20038  cxplea  20059  cxple2a  20062  ang180  20128  isosctrlem2  20135  cxp2lim  20287  amgm  20301  muval1  20387  dvdssqf  20392  mumullem2  20434  bcmono  20532  lgsneg  20574  lgsmod  20576  lgsdirprm  20584  lgsdir  20585  lgsdi  20587  nvmul0or  21226  shless  21954  shlej1  21955  pjspansn  22172  kbmul  22551  homco2  22573  kbass2  22713  snunioc  23282  eliccelico  23285  elicoelioo  23286  iocinioc2  23287  difioo  23290  xrge0npcan  23348  probinc  23639  cndprob01  23653  cvmsss2  23820  vdgrf  23906  dedekind  24097  dvdspw  24174  funsseq  24196  sltres  24389  brbtwn2  24605  colinearalglem1  24606  colinearalg  24610  axcgrtr  24615  axcontlem2  24665  cgrtriv  24697  5segofs  24701  btwntriv2  24707  btwnxfr  24751  segcon2  24800  brsegle2  24804  seglelin  24811  outsideofeu  24826  bpolydif  24862  sndw  25203  cmprtr  25499  rltrran  25517  rltrooo  25518  zerdivemp1  25539  fgsb2  25658  cmptdst  25671  cmptdst2  25674  limptlimpr2lem1  25677  limptlimpr2lem2  25678  flfnei2  25680  islimrs3  25684  usinuniopb  25697  mslb1  25710  lvsovso  25729  addcanri  25769  isder  25810  clscnc  26113  lppotos  26247  comppfsc  26410  blbnd  26614  rrndstprj2  26658  zerdivemp1x  26689  ofmpteq  26900  mzpsubst  26929  diophrw  26941  eldioph2lem1  26942  rencldnfi  27007  pellexlem2  27018  pellqrexplicit  27065  infmrgelbi  27066  rmxycomplete  27105  congadd  27156  acongeq  27173  jm2.19  27189  jm2.22  27191  jm2.20nn  27193  jm2.25lem1  27194  jm2.27  27204  jm3.1  27216  lmhmlnmsplit  27288  pwssplit0  27290  pwssplit1  27291  pwssplit4  27294  frlmsplit2  27346  frlmsslss2  27348  frlmup4  27356  lindff1  27393  lsslindf  27403  lsslinds  27404  islindf4  27411  hbtlem2  27431  dgraa0p  27457  pmtrfv  27498  pmtrmvd  27501  pmtrfb  27509  idomrootle  27614  hashgcdlem  27619  proot1hash  27622  fmul01  27813  iblioosinexp  27850  stoweidlem20  27872  stoweidlem22  27874  stoweidlem28  27880  stoweidlem34  27886  stoweidlem44  27896  stoweidlem51  27903  stoweidlem60  27912  wallispilem3  27919  s2f1o  28223  cyclispthon  28378  lubunNEW  29785  lsmsat  29820  lsatfixedN  29821  lssat  29828  lkrlsp  29914  lshpkrlem4  29925  op1cl  29997  cvrcon3b  30089  leat3  30107  atlen0  30122  atnle  30129  atlatmstc  30131  atlatle  30132  cvlcvr1  30151  cvlsupr2  30155  hlsupr2  30198  hlrelat2  30214  cvrexchlem  30230  cvratlem  30232  lnnat  30238  atexchcvrN  30251  1cvratlt  30285  1cvrjat  30286  3atlem3  30296  3atlem7  30300  llni2  30323  atcvrlln2  30330  llnexatN  30332  llncmp  30333  2llnmat  30335  2at0mat0  30336  2atnelpln  30355  llncvrlpln2  30368  2lplnmN  30370  2llnmj  30371  lplncmp  30373  lplnexatN  30374  2llnjaN  30377  lvoli3  30388  islvol2aN  30403  4atlem3a  30408  4atlem4a  30410  4atlem4b  30411  4atlem11  30420  4atlem12  30423  lplncvrlvol2  30426  lvolcmp  30428  2lplnmj  30433  islinei  30551  linepmap  30586  lneq2at  30589  2llnma3r  30599  elpaddn0  30611  elpaddatriN  30614  elpaddat  30615  paddcom  30624  paddss1  30628  paddss2  30629  paddasslem6  30636  paddasslem7  30637  paddasslem10  30640  paddasslem15  30645  pmodlem2  30658  pmodl42N  30662  pmapjoin  30663  atmod1i1m  30669  llnmod1i2  30671  llnexchb2lem  30679  polcon2bN  30731  pclfinclN  30761  poml4N  30764  poml6N  30766  osumcllem11N  30777  osumclN  30778  pmapojoinN  30779  pexmidlem2N  30782  pexmidlem3N  30783  pexmidlem4N  30784  pexmidlem6N  30786  pexmidlem7N  30787  pl42lem2N  30791  pl42lem3N  30792  pl42lem4N  30793  pl42N  30794  lhpexle3lem  30822  lhpmcvr3  30836  lhp2at0nle  30846  lhprelat3N  30851  lauteq  30906  lautco  30908  ltrncoidN  30939  ltrneq2  30959  ltrnnidn  30985  ltrnideq  30986  trlnle  30997  cdlemc  31008  cdlemd4  31012  cdlemd5  31013  cdlemd9  31017  cdlemd  31018  ltrneq3  31019  cdlemefrs29pre00  31206  cdlemefrs29cpre1  31209  cdlemefrs29clN  31210  cdlemefrs32fva  31211  cdlemefr29exN  31213  cdlemefr27cl  31214  cdlemefs27cl  31224  cdlemefs32sn1aw  31225  cdleme32fva  31248  cdleme32d  31255  cdleme32f  31257  cdleme32le  31258  cdleme40n  31279  cdleme41snaw  31287  cdleme17d3  31307  cdleme48fvg  31311  cdlemeg46fvcl  31317  cdlemeg46fgN  31345  cdleme48fgv  31349  ltrniotavalbN  31395  cdlemb3  31417  cdlemg15  31467  cdlemg17dN  31474  trlco  31538  cdlemg44b  31543  ltrncom  31549  trljco  31551  tendococl  31583  tendoplcl  31592  tendoplcom  31593  tendotr  31641  cdlemk36  31724  cdlemk35s-id  31749  cdlemk39s-id  31751  cdlemk19x  31754  cdlemk53b  31767  cdlemk55  31772  cdlemk35u  31775  cdlemk55u  31777  cdlemk39u  31779  cdlemk19u  31781  cdlemk56  31782  tendoex  31786  cdleml5N  31791  dihord2pre  32037  dihord6apre  32068  dihord5b  32071  dihord5apre  32074  dihord  32076  dihmeetlem1N  32102  dihmeetlem2N  32111  dihglbcpreN  32112  dihmeetbN  32115  dihmeetlem4preN  32118  dihmeetlem5  32120  dihmeetlem6  32121  dihmeetlem7N  32122  dihmeetlem10N  32128  dihmeetlem11N  32129  dihmeetlem12N  32130  dihmeetlem13N  32131  dihmeetlem15N  32133  dihmeetlem17N  32135  dihmeetlem18N  32136  dihmeetlem19N  32137  dihmeetALTN  32139  dih1dimatlem0  32140  dihlspsnssN  32144  dvh3dim2  32260
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator