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

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

Proof of Theorem simpl1
StepHypRef Expression
1 simp1 955 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ph )
21adantr 451 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  simpll1  994  simprl1  1000  simp1l1  1048  simp2l1  1054  simp3l1  1060  3anandirs  1284  rspc3ev  2894  cocan1  5801  weniso  5852  smogt  6384  smorndom  6385  omeulem1  6580  nnmord  6630  nnmword  6631  difsnen  6944  mapunen  7030  ac6sfi  7101  fipreima  7161  elfiun  7183  ordiso2  7230  wemaplem2  7262  wemapso  7266  en2eqpr  7637  indcardi  7668  fodomfi2  7687  iunfictbso  7741  infmap2  7844  cofsmo  7895  cfsmolem  7896  coftr  7899  fin23lem11  7943  fincssdom  7949  fin23lem26  7951  isf32lem9  7987  ac6num  8106  gchdomtri  8251  gchpwdom  8296  winainflem  8315  tskuni  8405  gruima  8424  gruf  8433  grudomon  8439  elnpi  8612  distrlem4pr  8650  prlem934  8657  addcan  8996  addcan2  8997  ltmul1a  9605  ledivmulOLD  9630  ledivmul2OLD  9634  suprleub  9718  supmul1  9719  infmrgelb  9734  suprzcl  10091  uzsupss  10310  xleadd1a  10573  xlesubadd  10583  xmulasslem3  10606  xlemul2a  10609  xadddilem  10614  xadddi2  10617  ixxun  10672  icoshftf1o  10759  lincmb01cmp  10777  iccf1o  10778  ltexp2a  11153  leexp2  11156  ltexp2r  11158  exple1  11161  expnlbnd2  11232  ccatass  11436  ccatopth  11462  limsupgre  11955  addcn2  12067  mulcn2  12069  dvdsadd2b  12571  dvdsmod  12585  oexpneg  12590  gcdass  12724  rplpwr  12735  rppwr  12736  coprmdvds2  12782  rpmulgcd2  12784  qredeq  12785  rpexp  12799  rpdvds  12803  prmdiveq  12854  odzdvds  12860  coprimeprodsq2  12863  pythagtriplem3  12871  pcdvdsb  12921  pcgcd1  12929  qexpz  12949  pockthg  12953  vdwnnlem1  13042  0ram  13067  ramz2  13071  lubss  14225  lubun  14227  clatleglb  14230  clatglbss  14231  mrelatglb  14287  issubmnd  14401  gsumccat  14464  frmdss2  14485  mulgneg  14585  mulgdirlem  14591  submmulg  14602  subgmulg  14635  nmzsubg  14658  ghmmulg  14695  odmodnn0  14855  odnncl  14860  odmod  14861  odmulgid  14867  odmulgeq  14870  odf1o1  14883  odf1o2  14884  odngen  14888  gexdvdsi  14894  pgpfi1  14906  odcau  14915  subgslw  14927  fislw  14936  lsmssv  14954  lsmless1x  14955  lsmless2x  14956  lsmsubm  14964  lsmmod  14984  lsmmod2  14985  efgred  15057  cntzcmn  15136  ghmplusg  15138  odadd1  15140  odadd2  15141  odadd  15142  lsmcomx  15148  gsumconst  15209  rng1eq0  15379  mulgass2  15387  isabvd  15585  lssintcl  15721  0lmhm  15797  lmhmvsca  15802  reslmhm2b  15811  lspfixed  15881  lspsnat  15898  lidldvgen  16007  issubassa  16064  psrplusgpropd  16313  coe1subfv  16343  coe1mul2  16346  xrsdsreclblem  16417  obselocv  16628  riinopn  16654  neiint  16841  topssnei  16861  restntr  16912  cnconst2  17011  cnrest2  17014  cnprest2  17018  cnpdis  17021  cnt0  17074  cnt1  17078  cnhaus  17082  ordthauslem  17111  cncmp  17119  fiuncmp  17131  sscmp  17132  hauscmp  17134  cnconn  17148  uncon  17155  nlly2i  17202  llynlly  17203  nllyidm  17215  ptrescn  17333  xkococnlem  17353  qtoptop2  17390  qtopss  17406  kqfvima  17421  r0cld  17429  ordthmeolem  17492  fbssint  17533  fmf  17640  fmss  17641  elfm  17642  rnelfmlem  17647  rnelfm  17648  fmco  17656  flimss2  17667  flimss1  17668  flimrest  17678  flftg  17691  cnpflf2  17695  cnpflf  17696  flfcnp  17699  supnfcls  17715  fclsss1  17717  fclsss2  17718  fcfnei  17730  fcfelbas  17731  cnpfcfi  17735  subgntr  17789  opnsubg  17790  cldsubg  17793  ghmcnp  17797  bldisj  17955  blgt0  17956  bl2in  17957  blss2  17959  blss  17972  xmetresbl  17983  lpbl  18049  blcld  18051  stdbdbl  18063  metcnp3  18086  metcnp2  18088  txmetcnp  18093  nmoix  18238  nmoeq0  18245  icoopnst  18437  iocopnst  18438  xrhmeo  18444  nmhmcn  18601  cphsqrcl2  18622  cphsqrcl3  18623  cfil3i  18695  caublcls  18734  bcthlem5  18750  pjth  18803  ovoliunlem2  18862  volun  18902  volsup2  18960  mbfimaopn2  19012  iblconst  19172  itgconst  19173  dvcnp2  19269  dvcn  19270  evlsval2  19404  deg1mul3le  19502  deg1tmle  19503  dvdsq1p  19546  ig1peu  19557  ig1pdvds  19562  coeid3  19622  dgrmulc  19652  efcvx  19825  tanord  19900  logdivlti  19971  logccv  20010  recxpcl  20022  cxpeq  20097  ang180  20112  isosctrlem2  20119  cxp2lim  20271  amgm  20285  muval1  20371  dvdssqf  20376  mumullem2  20418  mumul  20419  bcmono  20516  lgsfcl2  20541  lgsdilem  20561  lgsdirprm  20568  lgsdir  20569  lgsdi  20571  lgsne0  20572  gxcom  20936  gxnn0add  20941  nvmul0or  21210  ipval2lem2  21277  ipval2lem5  21283  lnomul  21338  shless  21938  shlej1  21939  pjspansn  22156  hoadddi  22383  kbmul  22535  homco2  22557  kbass2  22697  snunioc  23267  eliccelico  23270  elicoelioo  23271  iocinioc2  23272  iocinif  23274  xrge0adddir  23332  xrge0npcan  23333  probun  23622  probinc  23624  cndprob01  23638  pconpi1  23768  cvmsss2  23805  dvdspw  24103  br6  24114  br4  24115  frrlem4  24284  brbtwn2  24533  colinearalglem1  24534  colinearalg  24538  axcgrtr  24543  axsegconlem8  24552  axsegconlem9  24553  axsegconlem10  24554  axcontlem8  24599  axcontlem10  24601  cgrcomim  24612  cgrtriv  24625  cgrextend  24631  segconeq  24633  btwntriv2  24635  btwnintr  24642  btwnexch3  24643  btwnouttr2  24645  trisegint  24651  cgrsub  24668  cgrxfr  24678  btwnxfr  24679  lineext  24699  btwnconn1lem13  24722  btwnconn1lem14  24723  btwnconn3  24726  segcon2  24728  brsegle  24731  brsegle2  24732  segletr  24737  segleantisym  24738  seglelin  24739  outsideofeu  24754  lineunray  24770  lineelsb2  24771  areacirc  24931  sndw  25100  mapmapmap  25148  iscst4  25177  cmprtr  25396  cmprltr  25410  rltrran  25414  rltrooo  25415  zerdivemp1  25436  truni1  25505  efilcp  25552  fgsb2  25555  iscnp4  25563  cmptdst  25568  cmptdst2  25571  exopcopn  25572  limptlimpr2lem2  25575  usinuniopb  25594  lvsovso  25626  lvsovso3  25628  addcanri  25666  negveud  25668  negveudr  25669  mulmulvec  25687  distmlva  25688  isder  25707  cmpassoh  25801  idmon  25817  tartarmap  25888  idcatfun  25941  indcls2  25996  isconcl5a  26101  isconcl5ab  26102  lppotos  26144  ivthALT  26258  finlocfin  26299  cocanfo  26374  upixp  26403  ismtyima  26527  rrndstprj2  26555  zerdivemp1x  26586  mzprename  26827  eldioph2lem1  26839  lzunuz  26847  rencldnfi  26904  pellexlem2  26915  infmrgelbi  26963  pellfundglb  26970  pellfund14gap  26972  qirropth  26993  rmxycomplete  27002  congadd  27053  acongeq  27070  jm2.19  27086  jm2.23  27089  jm2.20nn  27090  jm2.27  27101  jm3.1  27113  aomclem6  27156  lnmepi  27183  lmhmfgsplit  27184  lmhmlnmsplit  27185  pwssplit1  27188  pwssplit3  27190  pwssplit4  27191  uvcresum  27242  frlmsslsp  27248  frlmup4  27253  enfixsn  27257  lindff1  27290  f1lindf  27292  lsslindf  27300  islindf4  27308  lbslcic  27311  hbtlem2  27328  hbtlem5  27332  dgraa0p  27354  pmtrfb  27406  psgnunilem4  27420  mhmvlin  27452  hashgcdlem  27516  proot1hash  27519  stoweidlem19  27768  stoweidlem20  27769  stoweidlem22  27771  stoweidlem28  27777  stoweidlem34  27783  stoweidlem44  27793  stoweidlem51  27800  stoweidlem60  27809  wallispilem3  27816  s2f1o  28091  bnj517  28917  bnj594  28944  lubunNEW  29163  lsatfixedN  29199  lssat  29206  eqlkr  29289  eqlkr2  29290  lkrlsp  29292  lshpkrlem4  29303  opposet  29372  cvrcon3b  29467  cvrcmp  29473  atlen0  29500  atnle  29507  atlatmstc  29509  cvlatexch3  29528  cvlsupr2  29533  hlsupr2  29576  hlrelat2  29592  cvrexchlem  29608  lnnat  29616  atcvrj2b  29621  atle  29625  atexchcvrN  29629  atbtwn  29635  athgt  29645  3dimlem3  29650  3dim1  29656  1cvratlt  29663  1cvrjat  29664  ps-1  29666  ps-2  29667  3atlem3  29674  3atlem5  29676  3atlem7  29678  llni  29697  llni2  29701  atcvrlln2  29708  llnexatN  29710  llncmp  29711  2llnmat  29713  2at0mat0  29714  lplni  29721  lplnnle2at  29730  2atnelpln  29733  lplnllnneN  29745  llncvrlpln2  29746  2lplnmN  29748  2llnmj  29749  lplncmp  29751  lplnexatN  29752  lplnexllnN  29753  2llnm3N  29758  lvoli  29764  lvoli3  29766  islvol2aN  29781  4atlem0a  29782  4atlem3  29785  4atlem3a  29786  4atlem4a  29788  4atlem4b  29789  4atlem4c  29790  4atlem4d  29791  4atlem10b  29794  4atlem11  29798  4atlem12  29801  lplncvrlvol2  29804  lvolcmp  29806  2lplnmj  29811  islinei  29929  pmapglbx  29958  linepmap  29964  lneq2at  29967  lnjatN  29969  lncvrat  29971  lncmp  29972  2llnma3r  29977  elpaddatriN  29992  elpaddat  29993  paddcom  30002  paddss1  30006  paddss2  30007  paddss12  30008  paddasslem6  30014  paddasslem7  30015  paddasslem8  30016  paddasslem9  30017  paddasslem15  30023  pmodlem2  30036  pmodl42N  30040  pmapjoin  30041  llnmod1i2  30049  2polcon4bN  30107  polcon2bN  30109  poml4N  30142  poml6N  30144  osumcllem1N  30145  osumcllem2N  30146  osumcllem11N  30155  osumclN  30156  pmapojoinN  30157  pexmidlem2N  30160  pexmidlem3N  30161  pexmidlem4N  30162  pexmidlem6N  30164  pexmidlem7N  30165  pl42lem2N  30169  pl42lem3N  30170  pl42lem4N  30171  pl42N  30172  lhpexle2lem  30198  lhpexle3lem  30200  lhpexle3  30201  lhpmcvr3  30214  lhp2at0nle  30224  lhprelat3N  30229  4atex  30265  4atex2  30266  lauteq  30284  lautco  30286  ltrncoidN  30317  ltrneq2  30337  ltrnnidn  30363  ltrnideq  30364  trlnid  30368  ltrnatlw  30372  trlnle  30375  trlval3  30376  trlval4  30377  cdlemc  30386  cdlemd5  30391  cdlemd9  30395  ltrneq3  30397  cdleme0moN  30414  cdleme20  30513  cdleme21j  30525  cdleme21  30526  cdleme27cl  30555  cdlemefrs29bpre0  30585  cdlemefs27cl  30602  cdlemefs32sn1aw  30603  cdleme43fsv1snlem  30609  cdleme32d  30633  cdleme32f  30635  cdleme32le  30636  cdleme35h2  30646  cdleme38n  30653  cdleme40m  30656  cdleme41snaw  30665  cdleme42ke  30674  cdleme17d3  30685  cdleme48fvg  30689  cdlemeg46fvcl  30695  cdlemeg46fgN  30723  cdleme48gfv1  30725  cdleme48fgv  30727  cdleme50trn3  30742  trlord  30758  ltrniotavalbN  30773  cdlemb3  30795  cdlemg6c  30809  cdlemg6  30812  cdlemg7N  30815  cdlemg8c  30818  cdlemg8  30820  cdlemg11a  30826  cdlemg11b  30831  cdlemg12e  30836  cdlemg15a  30844  cdlemg15  30845  cdlemg16  30846  cdlemg16z  30848  cdlemg16zz  30849  cdlemg17dN  30852  cdlemg18a  30867  cdlemg20  30874  cdlemg22  30876  cdlemg24  30877  cdlemg37  30878  cdlemg31d  30889  cdlemg29  30894  cdlemg33b  30896  cdlemg33  30900  cdlemg38  30904  cdlemg39  30905  cdlemg40  30906  trlco  30916  trlcone  30917  cdlemg42  30918  cdlemg44b  30921  ltrncom  30927  trljco  30929  tendococl  30961  tendoplcl  30970  tendoplcom  30971  cdlemj2  31011  cdlemj3  31012  tendoid0  31014  tendoconid  31018  tendotr  31019  cdlemk25-3  31093  cdlemk26b-3  31094  cdlemk34  31099  cdlemk36  31102  cdlemk38  31104  cdlemkid4  31123  cdlemk35s-id  31127  cdlemk39s-id  31129  cdlemk19x  31132  cdlemk53  31146  cdlemk55  31150  cdlemk55u  31155  cdlemk39u  31157  cdlemk19u  31159  cdlemk56  31160  tendoex  31164  cdleml3N  31167  cdleml5N  31169  tendospcanN  31213  cdlemm10N  31308  cdlemn11pre  31400  dihord2pre  31415  dihvalcqpre  31425  dihopelvalcpre  31438  dihord6apre  31446  dihord5b  31449  dihord5apre  31452  dihord  31454  dihmeetlem1N  31480  dihglblem5apreN  31481  dihglblem3N  31485  dihmeetlem2N  31489  dihglbcpreN  31490  dihmeetbN  31493  dihmeetlem4preN  31496  dihmeetlem5  31498  dihmeetlem7N  31500  dihmeetlem10N  31506  dihmeetlem11N  31507  dihmeetlem12N  31508  dihmeetlem13N  31509  dihmeetlem15N  31511  dihmeetlem16N  31512  dihmeetlem17N  31513  dihmeetlem18N  31514  dihmeetlem19N  31515  dihmeetALTN  31517  dih1dimatlem0  31518  dihlspsnssN  31522  dihlspsnat  31523  mapdh8ad  31969  hdmap14lem14  32074  hgmapvvlem3  32118
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