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  2907  cocan1  5817  weniso  5868  smogt  6400  smorndom  6401  omeulem1  6596  nnmord  6646  nnmword  6647  difsnen  6960  mapunen  7046  ac6sfi  7117  fipreima  7177  elfiun  7199  ordiso2  7246  wemaplem2  7278  wemapso  7282  en2eqpr  7653  indcardi  7684  fodomfi2  7703  iunfictbso  7757  infmap2  7860  cofsmo  7911  cfsmolem  7912  coftr  7915  fin23lem11  7959  fincssdom  7965  fin23lem26  7967  isf32lem9  8003  ac6num  8122  gchdomtri  8267  gchpwdom  8312  winainflem  8331  tskuni  8421  gruima  8440  gruf  8449  grudomon  8455  elnpi  8628  distrlem4pr  8666  prlem934  8673  addcan  9012  addcan2  9013  ltmul1a  9621  ledivmulOLD  9646  ledivmul2OLD  9650  suprleub  9734  supmul1  9735  infmrgelb  9750  suprzcl  10107  uzsupss  10326  xleadd1a  10589  xlesubadd  10599  xmulasslem3  10622  xlemul2a  10625  xadddilem  10630  xadddi2  10633  ixxun  10688  icoshftf1o  10775  lincmb01cmp  10793  iccf1o  10794  ltexp2a  11169  leexp2  11172  ltexp2r  11174  exple1  11177  expnlbnd2  11248  ccatass  11452  ccatopth  11478  limsupgre  11971  addcn2  12083  mulcn2  12085  dvdsadd2b  12587  dvdsmod  12601  oexpneg  12606  gcdass  12740  rplpwr  12751  rppwr  12752  coprmdvds2  12798  rpmulgcd2  12800  qredeq  12801  rpexp  12815  rpdvds  12819  prmdiveq  12870  odzdvds  12876  coprimeprodsq2  12879  pythagtriplem3  12887  pcdvdsb  12937  pcgcd1  12945  qexpz  12965  pockthg  12969  vdwnnlem1  13058  0ram  13083  ramz2  13087  lubss  14241  lubun  14243  clatleglb  14246  clatglbss  14247  mrelatglb  14303  issubmnd  14417  gsumccat  14480  frmdss2  14501  mulgneg  14601  mulgdirlem  14607  submmulg  14618  subgmulg  14651  nmzsubg  14674  ghmmulg  14711  odmodnn0  14871  odnncl  14876  odmod  14877  odmulgid  14883  odmulgeq  14886  odf1o1  14899  odf1o2  14900  odngen  14904  gexdvdsi  14910  pgpfi1  14922  odcau  14931  subgslw  14943  fislw  14952  lsmssv  14970  lsmless1x  14971  lsmless2x  14972  lsmsubm  14980  lsmmod  15000  lsmmod2  15001  efgred  15073  cntzcmn  15152  ghmplusg  15154  odadd1  15156  odadd2  15157  odadd  15158  lsmcomx  15164  gsumconst  15225  rng1eq0  15395  mulgass2  15403  isabvd  15601  lssintcl  15737  0lmhm  15813  lmhmvsca  15818  reslmhm2b  15827  lspfixed  15897  lspsnat  15914  lidldvgen  16023  issubassa  16080  psrplusgpropd  16329  coe1subfv  16359  coe1mul2  16362  xrsdsreclblem  16433  obselocv  16644  riinopn  16670  neiint  16857  topssnei  16877  restntr  16928  cnconst2  17027  cnrest2  17030  cnprest2  17034  cnpdis  17037  cnt0  17090  cnt1  17094  cnhaus  17098  ordthauslem  17127  cncmp  17135  fiuncmp  17147  sscmp  17148  hauscmp  17150  cnconn  17164  uncon  17171  nlly2i  17218  llynlly  17219  nllyidm  17231  ptrescn  17349  xkococnlem  17369  qtoptop2  17406  qtopss  17422  kqfvima  17437  r0cld  17445  ordthmeolem  17508  fbssint  17549  fmf  17656  fmss  17657  elfm  17658  rnelfmlem  17663  rnelfm  17664  fmco  17672  flimss2  17683  flimss1  17684  flimrest  17694  flftg  17707  cnpflf2  17711  cnpflf  17712  flfcnp  17715  supnfcls  17731  fclsss1  17733  fclsss2  17734  fcfnei  17746  fcfelbas  17747  cnpfcfi  17751  subgntr  17805  opnsubg  17806  cldsubg  17809  ghmcnp  17813  bldisj  17971  blgt0  17972  bl2in  17973  blss2  17975  blss  17988  xmetresbl  17999  lpbl  18065  blcld  18067  stdbdbl  18079  metcnp3  18102  metcnp2  18104  txmetcnp  18109  nmoix  18254  nmoeq0  18261  icoopnst  18453  iocopnst  18454  xrhmeo  18460  nmhmcn  18617  cphsqrcl2  18638  cphsqrcl3  18639  cfil3i  18711  caublcls  18750  bcthlem5  18766  pjth  18819  ovoliunlem2  18878  volun  18918  volsup2  18976  mbfimaopn2  19028  iblconst  19188  itgconst  19189  dvcnp2  19285  dvcn  19286  evlsval2  19420  deg1mul3le  19518  deg1tmle  19519  dvdsq1p  19562  ig1peu  19573  ig1pdvds  19578  coeid3  19638  dgrmulc  19668  efcvx  19841  tanord  19916  logdivlti  19987  logccv  20026  recxpcl  20038  cxpeq  20113  ang180  20128  isosctrlem2  20135  cxp2lim  20287  amgm  20301  muval1  20387  dvdssqf  20392  mumullem2  20434  mumul  20435  bcmono  20532  lgsfcl2  20557  lgsdilem  20577  lgsdirprm  20584  lgsdir  20585  lgsdi  20587  lgsne0  20588  gxcom  20952  gxnn0add  20957  nvmul0or  21226  ipval2lem2  21293  ipval2lem5  21299  lnomul  21354  shless  21954  shlej1  21955  pjspansn  22172  hoadddi  22399  kbmul  22551  homco2  22573  kbass2  22713  snunioc  23282  eliccelico  23285  elicoelioo  23286  iocinioc2  23287  iocinif  23289  xrge0adddir  23347  xrge0npcan  23348  probun  23637  probinc  23639  cndprob01  23653  pconpi1  23783  cvmsss2  23820  dvdspw  24174  br6  24185  br4  24186  frrlem4  24355  brbtwn2  24605  colinearalglem1  24606  colinearalg  24610  axcgrtr  24615  axsegconlem8  24624  axsegconlem9  24625  axsegconlem10  24626  axcontlem8  24671  axcontlem10  24673  cgrcomim  24684  cgrtriv  24697  cgrextend  24703  segconeq  24705  btwntriv2  24707  btwnintr  24714  btwnexch3  24715  btwnouttr2  24717  trisegint  24723  cgrsub  24740  cgrxfr  24750  btwnxfr  24751  lineext  24771  btwnconn1lem13  24794  btwnconn1lem14  24795  btwnconn3  24798  segcon2  24800  brsegle  24803  brsegle2  24804  segletr  24809  segleantisym  24810  seglelin  24811  outsideofeu  24826  lineunray  24842  lineelsb2  24843  areacirc  25034  sndw  25203  mapmapmap  25251  iscst4  25280  cmprtr  25499  cmprltr  25513  rltrran  25517  rltrooo  25518  zerdivemp1  25539  truni1  25608  efilcp  25655  fgsb2  25658  iscnp4  25666  cmptdst  25671  cmptdst2  25674  exopcopn  25675  limptlimpr2lem2  25678  usinuniopb  25697  lvsovso  25729  lvsovso3  25731  addcanri  25769  negveud  25771  negveudr  25772  mulmulvec  25790  distmlva  25791  isder  25810  cmpassoh  25904  idmon  25920  tartarmap  25991  idcatfun  26044  indcls2  26099  isconcl5a  26204  isconcl5ab  26205  lppotos  26247  ivthALT  26361  finlocfin  26402  cocanfo  26477  upixp  26506  ismtyima  26630  rrndstprj2  26658  zerdivemp1x  26689  mzprename  26930  eldioph2lem1  26942  lzunuz  26950  rencldnfi  27007  pellexlem2  27018  infmrgelbi  27066  pellfundglb  27073  pellfund14gap  27075  qirropth  27096  rmxycomplete  27105  congadd  27156  acongeq  27173  jm2.19  27189  jm2.23  27192  jm2.20nn  27193  jm2.27  27204  jm3.1  27216  aomclem6  27259  lnmepi  27286  lmhmfgsplit  27287  lmhmlnmsplit  27288  pwssplit1  27291  pwssplit3  27293  pwssplit4  27294  uvcresum  27345  frlmsslsp  27351  frlmup4  27356  enfixsn  27360  lindff1  27393  f1lindf  27395  lsslindf  27403  islindf4  27411  lbslcic  27414  hbtlem2  27431  hbtlem5  27435  dgraa0p  27457  pmtrfb  27509  psgnunilem4  27523  mhmvlin  27555  hashgcdlem  27619  proot1hash  27622  stoweidlem19  27871  stoweidlem20  27872  stoweidlem22  27874  stoweidlem28  27880  stoweidlem34  27886  stoweidlem44  27896  stoweidlem51  27903  stoweidlem60  27912  wallispilem3  27919  s2f1o  28223  bnj517  29233  bnj594  29260  lubunNEW  29785  lsatfixedN  29821  lssat  29828  eqlkr  29911  eqlkr2  29912  lkrlsp  29914  lshpkrlem4  29925  opposet  29994  cvrcon3b  30089  cvrcmp  30095  atlen0  30122  atnle  30129  atlatmstc  30131  cvlatexch3  30150  cvlsupr2  30155  hlsupr2  30198  hlrelat2  30214  cvrexchlem  30230  lnnat  30238  atcvrj2b  30243  atle  30247  atexchcvrN  30251  atbtwn  30257  athgt  30267  3dimlem3  30272  3dim1  30278  1cvratlt  30285  1cvrjat  30286  ps-1  30288  ps-2  30289  3atlem3  30296  3atlem5  30298  3atlem7  30300  llni  30319  llni2  30323  atcvrlln2  30330  llnexatN  30332  llncmp  30333  2llnmat  30335  2at0mat0  30336  lplni  30343  lplnnle2at  30352  2atnelpln  30355  lplnllnneN  30367  llncvrlpln2  30368  2lplnmN  30370  2llnmj  30371  lplncmp  30373  lplnexatN  30374  lplnexllnN  30375  2llnm3N  30380  lvoli  30386  lvoli3  30388  islvol2aN  30403  4atlem0a  30404  4atlem3  30407  4atlem3a  30408  4atlem4a  30410  4atlem4b  30411  4atlem4c  30412  4atlem4d  30413  4atlem10b  30416  4atlem11  30420  4atlem12  30423  lplncvrlvol2  30426  lvolcmp  30428  2lplnmj  30433  islinei  30551  pmapglbx  30580  linepmap  30586  lneq2at  30589  lnjatN  30591  lncvrat  30593  lncmp  30594  2llnma3r  30599  elpaddatriN  30614  elpaddat  30615  paddcom  30624  paddss1  30628  paddss2  30629  paddss12  30630  paddasslem6  30636  paddasslem7  30637  paddasslem8  30638  paddasslem9  30639  paddasslem15  30645  pmodlem2  30658  pmodl42N  30662  pmapjoin  30663  llnmod1i2  30671  2polcon4bN  30729  polcon2bN  30731  poml4N  30764  poml6N  30766  osumcllem1N  30767  osumcllem2N  30768  osumcllem11N  30777  osumclN  30778  pmapojoinN  30779  pexmidlem2N  30782  pexmidlem3N  30783  pexmidlem4N  30784  pexmidlem6N  30786  pexmidlem7N  30787  pl42lem2N  30791  pl42lem3N  30792  pl42lem4N  30793  pl42N  30794  lhpexle2lem  30820  lhpexle3lem  30822  lhpexle3  30823  lhpmcvr3  30836  lhp2at0nle  30846  lhprelat3N  30851  4atex  30887  4atex2  30888  lauteq  30906  lautco  30908  ltrncoidN  30939  ltrneq2  30959  ltrnnidn  30985  ltrnideq  30986  trlnid  30990  ltrnatlw  30994  trlnle  30997  trlval3  30998  trlval4  30999  cdlemc  31008  cdlemd5  31013  cdlemd9  31017  ltrneq3  31019  cdleme0moN  31036  cdleme20  31135  cdleme21j  31147  cdleme21  31148  cdleme27cl  31177  cdlemefrs29bpre0  31207  cdlemefs27cl  31224  cdlemefs32sn1aw  31225  cdleme43fsv1snlem  31231  cdleme32d  31255  cdleme32f  31257  cdleme32le  31258  cdleme35h2  31268  cdleme38n  31275  cdleme40m  31278  cdleme41snaw  31287  cdleme42ke  31296  cdleme17d3  31307  cdleme48fvg  31311  cdlemeg46fvcl  31317  cdlemeg46fgN  31345  cdleme48gfv1  31347  cdleme48fgv  31349  cdleme50trn3  31364  trlord  31380  ltrniotavalbN  31395  cdlemb3  31417  cdlemg6c  31431  cdlemg6  31434  cdlemg7N  31437  cdlemg8c  31440  cdlemg8  31442  cdlemg11a  31448  cdlemg11b  31453  cdlemg12e  31458  cdlemg15a  31466  cdlemg15  31467  cdlemg16  31468  cdlemg16z  31470  cdlemg16zz  31471  cdlemg17dN  31474  cdlemg18a  31489  cdlemg20  31496  cdlemg22  31498  cdlemg24  31499  cdlemg37  31500  cdlemg31d  31511  cdlemg29  31516  cdlemg33b  31518  cdlemg33  31522  cdlemg38  31526  cdlemg39  31527  cdlemg40  31528  trlco  31538  trlcone  31539  cdlemg42  31540  cdlemg44b  31543  ltrncom  31549  trljco  31551  tendococl  31583  tendoplcl  31592  tendoplcom  31593  cdlemj2  31633  cdlemj3  31634  tendoid0  31636  tendoconid  31640  tendotr  31641  cdlemk25-3  31715  cdlemk26b-3  31716  cdlemk34  31721  cdlemk36  31724  cdlemk38  31726  cdlemkid4  31745  cdlemk35s-id  31749  cdlemk39s-id  31751  cdlemk19x  31754  cdlemk53  31768  cdlemk55  31772  cdlemk55u  31777  cdlemk39u  31779  cdlemk19u  31781  cdlemk56  31782  tendoex  31786  cdleml3N  31789  cdleml5N  31791  tendospcanN  31835  cdlemm10N  31930  cdlemn11pre  32022  dihord2pre  32037  dihvalcqpre  32047  dihopelvalcpre  32060  dihord6apre  32068  dihord5b  32071  dihord5apre  32074  dihord  32076  dihmeetlem1N  32102  dihglblem5apreN  32103  dihglblem3N  32107  dihmeetlem2N  32111  dihglbcpreN  32112  dihmeetbN  32115  dihmeetlem4preN  32118  dihmeetlem5  32120  dihmeetlem7N  32122  dihmeetlem10N  32128  dihmeetlem11N  32129  dihmeetlem12N  32130  dihmeetlem13N  32131  dihmeetlem15N  32133  dihmeetlem16N  32134  dihmeetlem17N  32135  dihmeetlem18N  32136  dihmeetlem19N  32137  dihmeetALTN  32139  dih1dimatlem0  32140  dihlspsnssN  32144  dihlspsnat  32145  mapdh8ad  32591  hdmap14lem14  32696  hgmapvvlem3  32740
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