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  5800  soisores  5826  weniso  5854  knatar  5859  smorndom  6387  nnmord  6632  nnmword  6633  difsnen  6946  mapunen  7032  ac6sfi  7103  fipreima  7163  wemaplem2  7264  en2eqpr  7639  indcardi  7670  acndom  7680  fodomfi2  7689  infmap2  7846  cflim2  7891  coftr  7901  infpssrlem4  7934  fin23lem11  7945  fincssdom  7951  isf32lem9  7989  fin1a2lem9  8036  gchpwdom  8298  gruima  8426  prpssnq  8616  distrlem4pr  8652  addcan  8998  addcan2  8999  ledivmul2OLD  9636  supmul1  9721  uzsupss  10312  xaddass  10571  xleadd1a  10575  xlesubadd  10585  xmulasslem3  10608  xadddilem  10616  xadddi  10617  ixxun  10674  icoshftf1o  10761  modsubdir  11010  ltexp2a  11155  leexp2  11158  ltexp2r  11160  exple1  11163  expnlbnd2  11234  ccatass  11438  ccatopth  11464  limsuplt  11955  limsupgre  11957  addcn2  12069  mulcn2  12071  dvdsmod  12587  gcdass  12726  rplpwr  12737  rppwr  12738  rpmulgcd2  12786  rpexp  12801  rpdvds  12805  prmdiveq  12856  coprimeprodsq  12864  coprimeprodsq2  12865  pythagtriplem3  12873  pcdvdsb  12923  pcgcd1  12931  pcbc  12950  0ram  13069  ramz2  13073  ramub1lem1  13075  mremre  13508  mrieqv2d  13543  lubun  14229  issubmnd  14403  gsumccat  14466  frmdss2  14487  mulgnn0p1  14580  mulgnnsubcl  14581  mulgneg  14587  mulgdirlem  14593  nmzsubg  14660  ghmmulg  14697  odmodnn0  14857  oddvdsnn0  14861  odnncl  14862  odmod  14863  oddvds  14864  odeq  14867  odmulgid  14869  odmulg  14871  odmulgeq  14872  odbezout  14873  odf1o1  14885  odf1o2  14886  odngen  14890  odcau  14917  pgpssslw  14927  fislw  14938  lsmless1x  14957  lsmless2x  14958  lsmsubm  14966  lsmmod  14986  lsmmod2  14987  efgsfo  15050  cntzcmn  15138  odadd1  15142  odadd2  15143  odadd  15144  lsmcomx  15150  prdscmnd  15155  gsumconst  15211  rng1eq0  15381  cntzsubr  15579  isabvd  15587  lspss  15743  0lmhm  15799  reslmhm2  15812  lbspss  15837  lspfixed  15883  lsmcv  15896  lspsnat  15900  issubassa  16066  aspss  16074  coe1subfv  16345  coe1tm  16351  xrsdsreclblem  16419  obselocv  16630  neiint  16843  topssnei  16863  cnrest2  17016  cnprest2  17020  cnt0  17076  cnt1  17080  cnhaus  17084  cncmp  17121  fiuncmp  17133  sscmp  17134  hauscmp  17136  cnconn  17150  uncon  17157  kgen2ss  17252  ptpjopn  17308  ptrescn  17335  qtopss  17408  kqfvima  17423  r0cld  17431  cmphaushmeo  17493  fbssint  17535  fbasrn  17581  filuni  17582  ufilmax  17604  fin1aufil  17629  fmf  17642  fmss  17643  rnelfmlem  17649  rnelfm  17650  fmufil  17656  fmco  17658  flimss2  17669  flimss1  17670  flimrest  17680  cnpflf2  17697  cnpflf  17698  flfcnp  17701  lmflf  17702  supnfcls  17717  fclsss1  17719  fclsss2  17720  cnpfcfi  17737  subgntr  17791  opnsubg  17792  cldsubg  17795  bldisj  17957  blgt0  17958  bl2in  17959  blss2  17961  xbln0  17967  blss  17974  lpbl  18051  blcld  18053  blcls  18054  stdbdmopn  18066  metcnp2  18090  txmetcnp  18095  nmoix  18240  nmoi2  18241  nmoeq0  18247  nmotri  18250  metdsge  18355  metds0  18356  metdseq0  18360  icoopnst  18439  iccpnfhmeo  18445  xrhmeo  18446  nmhmcn  18603  cphsqrcl2  18624  cphsqrcl3  18625  fmcfil  18700  bcthlem5  18752  pjth  18805  ovolunnul  18861  volun  18904  voliunlem2  18910  itg2const  19097  iblconst  19174  itgconst  19175  limcvallem  19223  dvcnp2  19271  dvcn  19272  deg1mul3le  19504  deg1tmle  19505  ig1pdvds  19564  coe11  19636  dgrmulc  19654  dvply1  19666  aaliou2  19722  efcvx  19827  tanord  19902  logdivlti  19973  logccv  20012  recxpcl  20024  cxplea  20045  cxple2a  20048  ang180  20114  isosctrlem2  20121  cxp2lim  20273  amgm  20287  muval1  20373  dvdssqf  20378  mumullem2  20420  bcmono  20518  lgsneg  20560  lgsmod  20562  lgsdirprm  20570  lgsdir  20571  lgsdi  20573  nvmul0or  21212  shless  21940  shlej1  21941  pjspansn  22158  kbmul  22537  homco2  22559  kbass2  22699  snunioc  23269  eliccelico  23272  elicoelioo  23273  iocinioc2  23274  difioo  23277  xrge0npcan  23335  probinc  23626  cndprob01  23640  cvmsss2  23807  vdgrf  23893  dedekind  24084  dvdspw  24105  funsseq  24127  sltres  24320  brbtwn2  24535  colinearalglem1  24536  colinearalg  24540  axcgrtr  24545  axcontlem2  24595  cgrtriv  24627  5segofs  24631  btwntriv2  24637  btwnxfr  24681  segcon2  24730  brsegle2  24734  seglelin  24741  outsideofeu  24756  bpolydif  24792  sndw  25111  cmprtr  25407  rltrran  25425  rltrooo  25426  zerdivemp1  25447  fgsb2  25566  cmptdst  25579  cmptdst2  25582  limptlimpr2lem1  25585  limptlimpr2lem2  25586  flfnei2  25588  islimrs3  25592  usinuniopb  25605  mslb1  25618  lvsovso  25637  addcanri  25677  isder  25718  clscnc  26021  lppotos  26155  comppfsc  26318  blbnd  26522  rrndstprj2  26566  zerdivemp1x  26597  ofmpteq  26808  mzpsubst  26837  diophrw  26849  eldioph2lem1  26850  rencldnfi  26915  pellexlem2  26926  pellqrexplicit  26973  infmrgelbi  26974  rmxycomplete  27013  congadd  27064  acongeq  27081  jm2.19  27097  jm2.22  27099  jm2.20nn  27101  jm2.25lem1  27102  jm2.27  27112  jm3.1  27124  lmhmlnmsplit  27196  pwssplit0  27198  pwssplit1  27199  pwssplit4  27202  frlmsplit2  27254  frlmsslss2  27256  frlmup4  27264  lindff1  27301  lsslindf  27311  lsslinds  27312  islindf4  27319  hbtlem2  27339  dgraa0p  27365  pmtrfv  27406  pmtrmvd  27409  pmtrfb  27417  idomrootle  27522  hashgcdlem  27527  proot1hash  27530  fmul01  27721  iblioosinexp  27758  stoweidlem20  27780  stoweidlem22  27782  stoweidlem28  27788  stoweidlem34  27794  stoweidlem44  27804  stoweidlem51  27811  stoweidlem60  27820  wallispilem3  27827  s2f1o  28102  lubunNEW  29236  lsmsat  29271  lsatfixedN  29272  lssat  29279  lkrlsp  29365  lshpkrlem4  29376  op1cl  29448  cvrcon3b  29540  leat3  29558  atlen0  29573  atnle  29580  atlatmstc  29582  atlatle  29583  cvlcvr1  29602  cvlsupr2  29606  hlsupr2  29649  hlrelat2  29665  cvrexchlem  29681  cvratlem  29683  lnnat  29689  atexchcvrN  29702  1cvratlt  29736  1cvrjat  29737  3atlem3  29747  3atlem7  29751  llni2  29774  atcvrlln2  29781  llnexatN  29783  llncmp  29784  2llnmat  29786  2at0mat0  29787  2atnelpln  29806  llncvrlpln2  29819  2lplnmN  29821  2llnmj  29822  lplncmp  29824  lplnexatN  29825  2llnjaN  29828  lvoli3  29839  islvol2aN  29854  4atlem3a  29859  4atlem4a  29861  4atlem4b  29862  4atlem11  29871  4atlem12  29874  lplncvrlvol2  29877  lvolcmp  29879  2lplnmj  29884  islinei  30002  linepmap  30037  lneq2at  30040  2llnma3r  30050  elpaddn0  30062  elpaddatriN  30065  elpaddat  30066  paddcom  30075  paddss1  30079  paddss2  30080  paddasslem6  30087  paddasslem7  30088  paddasslem10  30091  paddasslem15  30096  pmodlem2  30109  pmodl42N  30113  pmapjoin  30114  atmod1i1m  30120  llnmod1i2  30122  llnexchb2lem  30130  polcon2bN  30182  pclfinclN  30212  poml4N  30215  poml6N  30217  osumcllem11N  30228  osumclN  30229  pmapojoinN  30230  pexmidlem2N  30233  pexmidlem3N  30234  pexmidlem4N  30235  pexmidlem6N  30237  pexmidlem7N  30238  pl42lem2N  30242  pl42lem3N  30243  pl42lem4N  30244  pl42N  30245  lhpexle3lem  30273  lhpmcvr3  30287  lhp2at0nle  30297  lhprelat3N  30302  lauteq  30357  lautco  30359  ltrncoidN  30390  ltrneq2  30410  ltrnnidn  30436  ltrnideq  30437  trlnle  30448  cdlemc  30459  cdlemd4  30463  cdlemd5  30464  cdlemd9  30468  cdlemd  30469  ltrneq3  30470  cdlemefrs29pre00  30657  cdlemefrs29cpre1  30660  cdlemefrs29clN  30661  cdlemefrs32fva  30662  cdlemefr29exN  30664  cdlemefr27cl  30665  cdlemefs27cl  30675  cdlemefs32sn1aw  30676  cdleme32fva  30699  cdleme32d  30706  cdleme32f  30708  cdleme32le  30709  cdleme40n  30730  cdleme41snaw  30738  cdleme17d3  30758  cdleme48fvg  30762  cdlemeg46fvcl  30768  cdlemeg46fgN  30796  cdleme48fgv  30800  ltrniotavalbN  30846  cdlemb3  30868  cdlemg15  30918  cdlemg17dN  30925  trlco  30989  cdlemg44b  30994  ltrncom  31000  trljco  31002  tendococl  31034  tendoplcl  31043  tendoplcom  31044  tendotr  31092  cdlemk36  31175  cdlemk35s-id  31200  cdlemk39s-id  31202  cdlemk19x  31205  cdlemk53b  31218  cdlemk55  31223  cdlemk35u  31226  cdlemk55u  31228  cdlemk39u  31230  cdlemk19u  31232  cdlemk56  31233  tendoex  31237  cdleml5N  31242  dihord2pre  31488  dihord6apre  31519  dihord5b  31522  dihord5apre  31525  dihord  31527  dihmeetlem1N  31553  dihmeetlem2N  31562  dihglbcpreN  31563  dihmeetbN  31566  dihmeetlem4preN  31569  dihmeetlem5  31571  dihmeetlem6  31572  dihmeetlem7N  31573  dihmeetlem10N  31579  dihmeetlem11N  31580  dihmeetlem12N  31581  dihmeetlem13N  31582  dihmeetlem15N  31584  dihmeetlem17N  31586  dihmeetlem18N  31587  dihmeetlem19N  31588  dihmeetALTN  31590  dih1dimatlem0  31591  dihlspsnssN  31595  dvh3dim2  31711
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