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

Theorem simpl1 960
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 957 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ph )
21adantr 452 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  simpll1  996  simprl1  1002  simp1l1  1050  simp2l1  1056  simp3l1  1062  3anandirs  1286  rspc3ev  3005  brcogw  4981  cocan1  5963  weniso  6014  smogt  6565  smorndom  6566  omeulem1  6761  nnmord  6811  nnmword  6812  difsnen  7126  mapunen  7212  ac6sfi  7287  fipreima  7347  elfiun  7370  ordiso2  7417  wemaplem2  7449  wemapso  7453  en2eqpr  7824  indcardi  7855  fodomfi2  7874  iunfictbso  7928  infmap2  8031  cofsmo  8082  cfsmolem  8083  coftr  8086  fin23lem11  8130  fincssdom  8136  fin23lem26  8138  isf32lem9  8174  ac6num  8292  gchdomtri  8437  gchpwdom  8482  winainflem  8501  tskuni  8591  gruima  8610  gruf  8619  grudomon  8625  elnpi  8798  distrlem4pr  8836  prlem934  8843  addcan  9182  addcan2  9183  ltmul1a  9791  ledivmulOLD  9816  ledivmul2OLD  9820  suprleub  9904  supmul1  9905  infmrgelb  9920  suprzcl  10281  uzsupss  10500  xleadd1a  10764  xlesubadd  10774  xmulasslem3  10797  xlemul2a  10800  xadddilem  10805  xadddi2  10808  ixxun  10864  icoshftf1o  10952  lincmb01cmp  10970  iccf1o  10971  ltexp2a  11358  leexp2  11361  ltexp2r  11363  exple1  11366  expnlbnd2  11437  ccatass  11677  ccatopth  11703  s2f1o  11790  limsupgre  12202  addcn2  12314  mulcn2  12316  dvdsadd2b  12819  dvdsmod  12833  oexpneg  12838  gcdass  12972  rplpwr  12983  rppwr  12984  coprmdvds2  13030  rpmulgcd2  13032  qredeq  13033  rpexp  13047  rpdvds  13051  prmdiveq  13102  odzdvds  13108  coprimeprodsq2  13111  pythagtriplem3  13119  pcdvdsb  13169  pcgcd1  13177  qexpz  13197  pockthg  13201  vdwnnlem1  13290  0ram  13315  ramz2  13319  lubss  14475  lubun  14477  clatleglb  14480  clatglbss  14481  mrelatglb  14537  issubmnd  14651  gsumccat  14714  frmdss2  14735  mulgneg  14835  mulgdirlem  14841  submmulg  14852  subgmulg  14885  nmzsubg  14908  ghmmulg  14945  odmodnn0  15105  odnncl  15110  odmod  15111  odmulgid  15117  odmulgeq  15120  odf1o1  15133  odf1o2  15134  odngen  15138  gexdvdsi  15144  pgpfi1  15156  odcau  15165  subgslw  15177  fislw  15186  lsmssv  15204  lsmless1x  15205  lsmless2x  15206  lsmsubm  15214  lsmmod  15234  lsmmod2  15235  efgred  15307  cntzcmn  15386  ghmplusg  15388  odadd1  15390  odadd2  15391  odadd  15392  lsmcomx  15398  gsumconst  15459  rng1eq0  15629  mulgass2  15637  isabvd  15835  lssintcl  15967  0lmhm  16043  lmhmvsca  16048  reslmhm2b  16057  lspfixed  16127  lspsnat  16144  lidldvgen  16253  issubassa  16310  psrplusgpropd  16556  coe1subfv  16586  coe1mul2  16589  xrsdsreclblem  16667  obselocv  16878  riinopn  16904  neiint  17091  topssnei  17111  restntr  17168  iscnp4  17249  cnconst2  17269  cnrest2  17272  cnprest2  17276  cnpdis  17279  cnt0  17332  cnt1  17336  cnhaus  17340  ordthauslem  17369  cncmp  17377  fiuncmp  17389  sscmp  17390  hauscmp  17392  cnconn  17406  uncon  17413  nlly2i  17460  llynlly  17461  nllyidm  17473  ptrescn  17592  xkococnlem  17612  qtoptop2  17652  qtopss  17668  kqfvima  17683  r0cld  17691  ordthmeolem  17754  fbssint  17791  fmf  17898  fmss  17899  elfm  17900  rnelfmlem  17905  rnelfm  17906  fmco  17914  flimss2  17925  flimss1  17926  flimrest  17936  flftg  17949  cnpflf2  17953  cnpflf  17954  flfcnp  17957  supnfcls  17973  fclsss1  17975  fclsss2  17976  fcfnei  17988  fcfelbas  17989  cnpfcfi  17993  subgntr  18057  opnsubg  18058  cldsubg  18061  ghmcnp  18065  utop2nei  18201  neipcfilu  18247  bldisj  18329  blgt0  18330  bl2in  18331  blss2  18333  blss  18346  xmetresbl  18357  lpbl  18423  blcld  18425  stdbdbl  18437  metcnp3  18460  metcnp2  18462  txmetcnp  18467  blval2  18482  nmoix  18634  nmoeq0  18641  icoopnst  18835  iocopnst  18836  xrhmeo  18842  nmhmcn  18999  cphsqrcl2  19020  cphsqrcl3  19021  cfil3i  19093  caublcls  19132  bcthlem5  19150  cmetcusp1  19174  pjth  19207  ovoliunlem2  19266  volun  19306  volsup2  19364  mbfimaopn2  19416  iblconst  19576  itgconst  19577  dvcnp2  19673  dvcn  19674  evlsval2  19808  deg1mul3le  19906  deg1tmle  19907  dvdsq1p  19950  ig1peu  19961  ig1pdvds  19966  coeid3  20026  dgrmulc  20056  efcvx  20232  tanord  20307  logdivlti  20382  logccv  20421  recxpcl  20433  cxpeq  20508  ang180  20523  isosctrlem2  20530  cxp2lim  20682  amgm  20696  muval1  20783  dvdssqf  20788  mumullem2  20830  mumul  20831  bcmono  20928  lgsfcl2  20953  lgsdilem  20973  lgsdirprm  20980  lgsdir  20981  lgsdi  20983  lgsne0  20984  2pthon  21450  gxcom  21705  gxnn0add  21710  zerdivemp1  21870  nvmul0or  21981  ipval2lem2  22048  ipval2lem5  22054  lnomul  22109  shless  22709  shlej1  22710  pjspansn  22927  hoadddi  23154  kbmul  23306  homco2  23328  kbass2  23468  snunioc  23973  eliccelico  23976  elicoelioo  23977  iocinioc2  23978  iocinif  23980  ress0g  24021  xrge0adddir  24044  xrge0npcan  24045  rhmdvdsr  24072  fmcncfil  24121  zrhnm  24154  qqhnm  24173  measvunilem  24360  volfiniune  24380  dya2iocnrect  24425  probun  24456  probinc  24458  cndprob01  24472  pconpi1  24703  cvmsss2  24740  ntrivcvgmul  25009  dvdspw  25127  br6  25138  br4  25139  frrlem4  25308  brbtwn2  25558  colinearalglem1  25559  colinearalg  25563  axcgrtr  25568  axsegconlem8  25577  axsegconlem9  25578  axsegconlem10  25579  axcontlem8  25624  axcontlem10  25626  cgrcomim  25637  cgrtriv  25650  cgrextend  25656  segconeq  25658  btwntriv2  25660  btwnintr  25667  btwnexch3  25668  btwnouttr2  25670  trisegint  25676  cgrsub  25693  cgrxfr  25703  btwnxfr  25704  lineext  25724  btwnconn1lem13  25747  btwnconn1lem14  25748  btwnconn3  25751  segcon2  25753  brsegle  25756  brsegle2  25757  segletr  25762  segleantisym  25763  seglelin  25764  outsideofeu  25779  lineunray  25795  lineelsb2  25796  areacirc  25988  ivthALT  26029  finlocfin  26070  cocanfo  26110  upixp  26122  ismtyima  26203  rrndstprj2  26231  zerdivemp1x  26262  mzprename  26497  eldioph2lem1  26509  lzunuz  26517  rencldnfi  26573  pellexlem2  26584  infmrgelbi  26632  pellfundglb  26639  pellfund14gap  26641  qirropth  26662  rmxycomplete  26671  congadd  26722  acongeq  26739  jm2.19  26755  jm2.23  26758  jm2.20nn  26759  jm2.27  26770  jm3.1  26782  aomclem6  26825  lnmepi  26852  lmhmfgsplit  26853  lmhmlnmsplit  26854  pwssplit1  26857  pwssplit3  26859  pwssplit4  26860  uvcresum  26911  frlmsslsp  26917  frlmup4  26922  enfixsn  26926  lindff1  26959  f1lindf  26961  lsslindf  26969  islindf4  26977  lbslcic  26980  hbtlem2  26997  hbtlem5  27001  dgraa0p  27023  pmtrfb  27075  psgnunilem4  27089  mhmvlin  27121  hashgcdlem  27185  proot1hash  27188  stoweidlem19  27436  stoweidlem20  27437  stoweidlem22  27439  stoweidlem28  27445  stoweidlem34  27451  stoweidlem44  27461  stoweidlem60  27477  wallispilem3  27484  bnj517  28594  bnj594  28621  lubunNEW  29088  lsatfixedN  29124  lssat  29131  eqlkr  29214  eqlkr2  29215  lkrlsp  29217  lshpkrlem4  29228  opposet  29297  cvrcon3b  29392  cvrcmp  29398  atlen0  29425  atnle  29432  atlatmstc  29434  cvlatexch3  29453  cvlsupr2  29458  hlsupr2  29501  hlrelat2  29517  cvrexchlem  29533  lnnat  29541  atcvrj2b  29546  atle  29550  atexchcvrN  29554  atbtwn  29560  athgt  29570  3dimlem3  29575  3dim1  29581  1cvratlt  29588  1cvrjat  29589  ps-1  29591  ps-2  29592  3atlem3  29599  3atlem5  29601  3atlem7  29603  llni  29622  llni2  29626  atcvrlln2  29633  llnexatN  29635  llncmp  29636  2llnmat  29638  2at0mat0  29639  lplni  29646  lplnnle2at  29655  2atnelpln  29658  lplnllnneN  29670  llncvrlpln2  29671  2lplnmN  29673  2llnmj  29674  lplncmp  29676  lplnexatN  29677  lplnexllnN  29678  2llnm3N  29683  lvoli  29689  lvoli3  29691  islvol2aN  29706  4atlem0a  29707  4atlem3  29710  4atlem3a  29711  4atlem4a  29713  4atlem4b  29714  4atlem4c  29715  4atlem4d  29716  4atlem10b  29719  4atlem11  29723  4atlem12  29726  lplncvrlvol2  29729  lvolcmp  29731  2lplnmj  29736  islinei  29854  pmapglbx  29883  linepmap  29889  lneq2at  29892  lnjatN  29894  lncvrat  29896  lncmp  29897  2llnma3r  29902  elpaddatriN  29917  elpaddat  29918  paddcom  29927  paddss1  29931  paddss2  29932  paddss12  29933  paddasslem6  29939  paddasslem7  29940  paddasslem8  29941  paddasslem9  29942  paddasslem15  29948  pmodlem2  29961  pmodl42N  29965  pmapjoin  29966  llnmod1i2  29974  2polcon4bN  30032  polcon2bN  30034  poml4N  30067  poml6N  30069  osumcllem1N  30070  osumcllem2N  30071  osumcllem11N  30080  osumclN  30081  pmapojoinN  30082  pexmidlem2N  30085  pexmidlem3N  30086  pexmidlem4N  30087  pexmidlem6N  30089  pexmidlem7N  30090  pl42lem2N  30094  pl42lem3N  30095  pl42lem4N  30096  pl42N  30097  lhpexle2lem  30123  lhpexle3lem  30125  lhpexle3  30126  lhpmcvr3  30139  lhp2at0nle  30149  lhprelat3N  30154  4atex  30190  4atex2  30191  lauteq  30209  lautco  30211  ltrncoidN  30242  ltrneq2  30262  ltrnnidn  30288  ltrnideq  30289  trlnid  30293  ltrnatlw  30297  trlnle  30300  trlval3  30301  trlval4  30302  cdlemc  30311  cdlemd5  30316  cdlemd9  30320  ltrneq3  30322  cdleme0moN  30339  cdleme20  30438  cdleme21j  30450  cdleme21  30451  cdleme27cl  30480  cdlemefrs29bpre0  30510  cdlemefs27cl  30527  cdlemefs32sn1aw  30528  cdleme43fsv1snlem  30534  cdleme32d  30558  cdleme32f  30560  cdleme32le  30561  cdleme35h2  30571  cdleme38n  30578  cdleme40m  30581  cdleme41snaw  30590  cdleme42ke  30599  cdleme17d3  30610  cdleme48fvg  30614  cdlemeg46fvcl  30620  cdlemeg46fgN  30648  cdleme48gfv1  30650  cdleme48fgv  30652  cdleme50trn3  30667  trlord  30683  ltrniotavalbN  30698  cdlemb3  30720  cdlemg6c  30734  cdlemg6  30737  cdlemg7N  30740  cdlemg8c  30743  cdlemg8  30745  cdlemg11a  30751  cdlemg11b  30756  cdlemg12e  30761  cdlemg15a  30769  cdlemg15  30770  cdlemg16  30771  cdlemg16z  30773  cdlemg16zz  30774  cdlemg17dN  30777  cdlemg18a  30792  cdlemg20  30799  cdlemg22  30801  cdlemg24  30802  cdlemg37  30803  cdlemg31d  30814  cdlemg29  30819  cdlemg33b  30821  cdlemg33  30825  cdlemg38  30829  cdlemg39  30830  cdlemg40  30831  trlco  30841  trlcone  30842  cdlemg42  30843  cdlemg44b  30846  ltrncom  30852  trljco  30854  tendococl  30886  tendoplcl  30895  tendoplcom  30896  cdlemj2  30936  cdlemj3  30937  tendoid0  30939  tendoconid  30943  tendotr  30944  cdlemk25-3  31018  cdlemk26b-3  31019  cdlemk34  31024  cdlemk36  31027  cdlemk38  31029  cdlemkid4  31048  cdlemk35s-id  31052  cdlemk39s-id  31054  cdlemk19x  31057  cdlemk53  31071  cdlemk55  31075  cdlemk55u  31080  cdlemk39u  31082  cdlemk19u  31084  cdlemk56  31085  tendoex  31089  cdleml3N  31092  cdleml5N  31094  tendospcanN  31138  cdlemm10N  31233  cdlemn11pre  31325  dihord2pre  31340  dihvalcqpre  31350  dihopelvalcpre  31363  dihord6apre  31371  dihord5b  31374  dihord5apre  31377  dihord  31379  dihmeetlem1N  31405  dihglblem5apreN  31406  dihglblem3N  31410  dihmeetlem2N  31414  dihglbcpreN  31415  dihmeetbN  31418  dihmeetlem4preN  31421  dihmeetlem5  31423  dihmeetlem7N  31425  dihmeetlem10N  31431  dihmeetlem11N  31432  dihmeetlem12N  31433  dihmeetlem13N  31434  dihmeetlem15N  31436  dihmeetlem16N  31437  dihmeetlem17N  31438  dihmeetlem18N  31439  dihmeetlem19N  31440  dihmeetALTN  31442  dih1dimatlem0  31443  dihlspsnssN  31447  dihlspsnat  31448  mapdh8ad  31894  hdmap14lem14  31999  hgmapvvlem3  32043
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