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

Theorem simpl3 962
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 959 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ch )
21adantr 452 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  simpll3  998  simprl3  1004  simp1l3  1052  simp2l3  1058  simp3l3  1064  3anandirs  1286  fcofo  6013  soisores  6039  weniso  6067  knatar  6072  smorndom  6622  nnmord  6867  nnmword  6868  difsnen  7182  mapunen  7268  ac6sfi  7343  fipreima  7404  wemaplem2  7508  en2eqpr  7883  indcardi  7914  acndom  7924  fodomfi2  7933  infmap2  8090  cflim2  8135  coftr  8145  infpssrlem4  8178  fin23lem11  8189  fincssdom  8195  isf32lem9  8233  fin1a2lem9  8280  gchpwdom  8541  gruima  8669  prpssnq  8859  distrlem4pr  8895  addcan  9242  addcan2  9243  ledivmul2OLD  9880  supmul1  9965  uzsupss  10560  xaddass  10820  xleadd1a  10824  xlesubadd  10834  xmulasslem3  10857  xadddilem  10865  xadddi  10866  ixxun  10924  icoshftf1o  11012  modsubdir  11277  ltexp2a  11423  leexp2  11426  ltexp2r  11428  exple1  11431  expnlbnd2  11502  hashtpg  11683  ccatass  11742  ccatopth  11768  s2f1o  11855  limsuplt  12265  limsupgre  12267  addcn2  12379  mulcn2  12381  dvdsmod  12898  gcdass  13037  rplpwr  13048  rppwr  13049  rpmulgcd2  13097  rpexp  13112  rpdvds  13116  prmdiveq  13167  coprimeprodsq  13175  coprimeprodsq2  13176  pythagtriplem3  13184  pcdvdsb  13234  pcgcd1  13242  pcbc  13261  0ram  13380  ramz2  13384  ramub1lem1  13386  mremre  13821  mrieqv2d  13856  lubun  14542  issubmnd  14716  gsumccat  14779  frmdss2  14800  mulgnn0p1  14893  mulgnnsubcl  14894  mulgneg  14900  mulgdirlem  14906  nmzsubg  14973  ghmmulg  15010  odmodnn0  15170  oddvdsnn0  15174  odnncl  15175  odmod  15176  oddvds  15177  odeq  15180  odmulgid  15182  odmulg  15184  odmulgeq  15185  odbezout  15186  odf1o1  15198  odf1o2  15199  odngen  15203  odcau  15230  pgpssslw  15240  fislw  15251  lsmless1x  15270  lsmless2x  15271  lsmsubm  15279  lsmmod  15299  lsmmod2  15300  efgsfo  15363  cntzcmn  15451  odadd1  15455  odadd2  15456  odadd  15457  lsmcomx  15463  prdscmnd  15468  gsumconst  15524  rng1eq0  15694  cntzsubr  15892  isabvd  15900  lspss  16052  0lmhm  16108  reslmhm2  16121  lbspss  16146  lspfixed  16192  lsmcv  16205  lspsnat  16209  issubassa  16375  aspss  16383  coe1subfv  16651  coe1tm  16657  xrsdsreclblem  16736  obselocv  16947  neiint  17160  topssnei  17180  cnrest2  17342  cnprest2  17346  cnt0  17402  cnt1  17406  cnhaus  17410  cncmp  17447  fiuncmp  17459  sscmp  17460  hauscmp  17462  cnconn  17477  uncon  17484  kgen2ss  17579  ptpjopn  17636  ptrescn  17663  qtopss  17739  kqfvima  17754  r0cld  17762  cmphaushmeo  17824  fbssint  17862  fbasrn  17908  filuni  17909  ufilmax  17931  fin1aufil  17956  fmf  17969  fmss  17970  rnelfmlem  17976  rnelfm  17977  fmufil  17983  fmco  17985  flimss2  17996  flimss1  17997  flimrest  18007  cnpflf2  18024  cnpflf  18025  flfcnp  18028  lmflf  18029  supnfcls  18044  fclsss1  18046  fclsss2  18047  cnpfcfi  18064  subgntr  18128  opnsubg  18129  cldsubg  18132  ustuqtop1  18263  ucncn  18307  bldisj  18420  blgt0  18421  bl2in  18422  blss2ps  18425  blss2  18426  xbln0  18436  blssps  18446  blss  18447  lpbl  18525  blcld  18527  blcls  18528  stdbdmopn  18540  metcnp2  18564  txmetcnp  18569  blval2  18597  restmetu  18609  nmoix  18755  nmoi2  18756  nmoeq0  18762  nmotri  18765  metdsge  18871  metds0  18872  metdseq0  18876  icoopnst  18956  iccpnfhmeo  18962  xrhmeo  18963  nmhmcn  19120  cphsqrcl2  19141  cphsqrcl3  19142  fmcfil  19217  bcthlem5  19273  cmetcusp1OLD  19297  cmetcusp1  19298  pjth  19332  ovolunnul  19388  volun  19431  voliunlem2  19437  itg2const  19624  iblconst  19701  itgconst  19702  limcvallem  19750  dvcnp2  19798  dvcn  19799  deg1mul3le  20031  deg1tmle  20032  ig1pdvds  20091  coe11  20163  dgrmulc  20181  dvply1  20193  aaliou2  20249  efcvx  20357  tanord  20432  logdivlti  20507  logccv  20546  recxpcl  20558  cxplea  20579  cxple2a  20582  ang180  20648  isosctrlem2  20655  cxp2lim  20807  amgm  20821  muval1  20908  dvdssqf  20913  mumullem2  20955  bcmono  21053  lgsneg  21095  lgsmod  21097  lgsdirprm  21105  lgsdir  21106  lgsdi  21108  cyclispthon  21612  vdgrfif  21662  zerdivemp1  22014  nvmul0or  22125  shless  22853  shlej1  22854  pjspansn  23071  kbmul  23450  homco2  23472  kbass2  23612  snunioc  24129  eliccelico  24132  elicoelioo  24133  iocinioc2  24134  difioo  24137  xrge0npcan  24208  isarchi2  24247  pstmfval  24283  fmcncfil  24309  zrhnm  24345  qqhnm  24366  volfiniune  24578  probinc  24671  cndprob01  24685  cvmsss2  24953  dedekind  25179  binomrisefac  25350  dvdspw  25361  funsseq  25385  sltres  25611  brbtwn2  25836  colinearalglem1  25837  colinearalg  25841  axcgrtr  25846  axcontlem2  25896  cgrtriv  25928  5segofs  25932  btwntriv2  25938  btwnxfr  25982  segcon2  26031  brsegle2  26035  seglelin  26042  outsideofeu  26057  bpolydif  26093  mblfinlem  26234  comppfsc  26378  blbnd  26487  rrndstprj2  26531  zerdivemp1x  26562  ofmpteq  26767  mzpsubst  26796  diophrw  26808  eldioph2lem1  26809  rencldnfi  26873  pellexlem2  26884  pellqrexplicit  26931  infmrgelbi  26932  rmxycomplete  26971  congadd  27022  acongeq  27039  jm2.19  27055  jm2.22  27057  jm2.20nn  27059  jm2.25lem1  27060  jm2.27  27070  jm3.1  27082  lmhmlnmsplit  27153  pwssplit0  27155  pwssplit1  27156  pwssplit4  27159  frlmsplit2  27211  frlmsslss2  27213  frlmup4  27221  lindff1  27258  lsslindf  27268  lsslinds  27269  islindf4  27276  hbtlem2  27296  dgraa0p  27322  pmtrfv  27363  pmtrmvd  27366  pmtrfb  27374  idomrootle  27479  hashgcdlem  27484  proot1hash  27487  fmul01  27677  ibliccsinexp  27712  iblioosinexp  27714  stoweidlem20  27736  stoweidlem22  27738  stoweidlem34  27750  stoweidlem44  27760  stoweidlem60  27776  wallispilem3  27783  fzo1fzo0n0  28111  modaddmulmod  28136  modifeq2int  28139  swrdnd  28154  swrdvalodmlem1  28159  swrdccatin12lem3a  28174  swrdccatin12  28180  swrdccat3  28181  4cyclusnfrgra  28346  lubunNEW  29708  lsmsat  29743  lsatfixedN  29744  lssat  29751  lkrlsp  29837  lshpkrlem4  29848  op1cl  29920  cvrcon3b  30012  leat3  30030  atlen0  30045  atnle  30052  atlatmstc  30054  atlatle  30055  cvlcvr1  30074  cvlsupr2  30078  hlsupr2  30121  hlrelat2  30137  cvrexchlem  30153  cvratlem  30155  lnnat  30161  atexchcvrN  30174  1cvratlt  30208  1cvrjat  30209  3atlem3  30219  3atlem7  30223  llni2  30246  atcvrlln2  30253  llnexatN  30255  llncmp  30256  2llnmat  30258  2at0mat0  30259  2atnelpln  30278  llncvrlpln2  30291  2lplnmN  30293  2llnmj  30294  lplncmp  30296  lplnexatN  30297  2llnjaN  30300  lvoli3  30311  islvol2aN  30326  4atlem3a  30331  4atlem4a  30333  4atlem4b  30334  4atlem11  30343  4atlem12  30346  lplncvrlvol2  30349  lvolcmp  30351  2lplnmj  30356  islinei  30474  linepmap  30509  lneq2at  30512  2llnma3r  30522  elpaddn0  30534  elpaddatriN  30537  elpaddat  30538  paddcom  30547  paddss1  30551  paddss2  30552  paddasslem6  30559  paddasslem7  30560  paddasslem10  30563  paddasslem15  30568  pmodlem2  30581  pmodl42N  30585  pmapjoin  30586  atmod1i1m  30592  llnmod1i2  30594  llnexchb2lem  30602  polcon2bN  30654  pclfinclN  30684  poml4N  30687  poml6N  30689  osumcllem11N  30700  osumclN  30701  pmapojoinN  30702  pexmidlem2N  30705  pexmidlem3N  30706  pexmidlem4N  30707  pexmidlem6N  30709  pexmidlem7N  30710  pl42lem2N  30714  pl42lem3N  30715  pl42lem4N  30716  pl42N  30717  lhpexle3lem  30745  lhpmcvr3  30759  lhp2at0nle  30769  lhprelat3N  30774  lauteq  30829  lautco  30831  ltrncoidN  30862  ltrneq2  30882  ltrnnidn  30908  ltrnideq  30909  trlnle  30920  cdlemc  30931  cdlemd4  30935  cdlemd5  30936  cdlemd9  30940  cdlemd  30941  ltrneq3  30942  cdlemefrs29pre00  31129  cdlemefrs29cpre1  31132  cdlemefrs29clN  31133  cdlemefrs32fva  31134  cdlemefr29exN  31136  cdlemefr27cl  31137  cdlemefs27cl  31147  cdlemefs32sn1aw  31148  cdleme32fva  31171  cdleme32d  31178  cdleme32f  31180  cdleme32le  31181  cdleme40n  31202  cdleme41snaw  31210  cdleme17d3  31230  cdleme48fvg  31234  cdlemeg46fvcl  31240  cdlemeg46fgN  31268  cdleme48fgv  31272  ltrniotavalbN  31318  cdlemb3  31340  cdlemg15  31390  cdlemg17dN  31397  trlco  31461  cdlemg44b  31466  ltrncom  31472  trljco  31474  tendococl  31506  tendoplcl  31515  tendoplcom  31516  tendotr  31564  cdlemk36  31647  cdlemk35s-id  31672  cdlemk39s-id  31674  cdlemk19x  31677  cdlemk53b  31690  cdlemk55  31695  cdlemk35u  31698  cdlemk55u  31700  cdlemk39u  31702  cdlemk19u  31704  cdlemk56  31705  tendoex  31709  cdleml5N  31714  dihord2pre  31960  dihord6apre  31991  dihord5b  31994  dihord5apre  31997  dihord  31999  dihmeetlem1N  32025  dihmeetlem2N  32034  dihglbcpreN  32035  dihmeetbN  32038  dihmeetlem4preN  32041  dihmeetlem5  32043  dihmeetlem6  32044  dihmeetlem7N  32045  dihmeetlem10N  32051  dihmeetlem11N  32052  dihmeetlem12N  32053  dihmeetlem13N  32054  dihmeetlem15N  32056  dihmeetlem17N  32058  dihmeetlem18N  32059  dihmeetlem19N  32060  dihmeetALTN  32062  dih1dimatlem0  32063  dihlspsnssN  32067  dvh3dim2  32183
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator