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

Theorem simpl1 961
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 958 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ph )
21adantr 453 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  simpll1  997  simprl1  1003  simp1l1  1051  simp2l1  1057  simp3l1  1063  3anandirs  1287  rspc3ev  3064  brcogw  5044  cocan1  6027  weniso  6078  smogt  6632  smorndom  6633  omeulem1  6828  nnmord  6878  nnmword  6879  difsnen  7193  mapunen  7279  ac6sfi  7354  fipreima  7415  elfiun  7438  ordiso2  7487  wemaplem2  7519  wemapso  7523  en2eqpr  7896  indcardi  7927  fodomfi2  7946  iunfictbso  8000  infmap2  8103  cofsmo  8154  cfsmolem  8155  coftr  8158  fin23lem11  8202  fincssdom  8208  fin23lem26  8210  isf32lem9  8246  ac6num  8364  gchdomtri  8509  gchpwdom  8550  winainflem  8573  tskuni  8663  gruima  8682  gruf  8691  grudomon  8697  elnpi  8870  distrlem4pr  8908  prlem934  8915  addcan  9255  addcan2  9256  ltmul1a  9864  ledivmulOLD  9889  ledivmul2OLD  9893  suprleub  9977  supmul1  9978  infmrgelb  9993  suprzcl  10354  uzsupss  10573  xleadd1a  10837  xlesubadd  10847  xmulasslem3  10870  xlemul2a  10873  xadddilem  10878  xadddi2  10881  ixxun  10937  icoshftf1o  11025  lincmb01cmp  11043  iccf1o  11044  ltexp2a  11436  leexp2  11439  ltexp2r  11441  exple1  11444  expnlbnd2  11515  ccatass  11755  ccatopth  11781  s2f1o  11868  limsupgre  12280  addcn2  12392  mulcn2  12394  dvdsadd2b  12897  dvdsmod  12911  oexpneg  12916  gcdass  13050  rplpwr  13061  rppwr  13062  coprmdvds2  13108  rpmulgcd2  13110  qredeq  13111  rpexp  13125  rpdvds  13129  prmdiveq  13180  odzdvds  13186  coprimeprodsq2  13189  pythagtriplem3  13197  pcdvdsb  13247  pcgcd1  13255  qexpz  13275  pockthg  13279  vdwnnlem1  13368  0ram  13393  ramz2  13397  lubss  14553  lubun  14555  clatleglb  14558  clatglbss  14559  mrelatglb  14615  issubmnd  14729  gsumccat  14792  frmdss2  14813  mulgneg  14913  mulgdirlem  14919  submmulg  14930  subgmulg  14963  nmzsubg  14986  ghmmulg  15023  odmodnn0  15183  odnncl  15188  odmod  15189  odmulgid  15195  odmulgeq  15198  odf1o1  15211  odf1o2  15212  odngen  15216  gexdvdsi  15222  pgpfi1  15234  odcau  15243  subgslw  15255  fislw  15264  lsmssv  15282  lsmless1x  15283  lsmless2x  15284  lsmsubm  15292  lsmmod  15312  lsmmod2  15313  efgred  15385  cntzcmn  15464  ghmplusg  15466  odadd1  15468  odadd2  15469  odadd  15470  lsmcomx  15476  gsumconst  15537  rng1eq0  15707  mulgass2  15715  isabvd  15913  lssintcl  16045  0lmhm  16121  lmhmvsca  16126  reslmhm2b  16135  lspfixed  16205  lspsnat  16222  lidldvgen  16331  issubassa  16388  psrplusgpropd  16634  coe1subfv  16664  coe1mul2  16667  xrsdsreclblem  16749  obselocv  16960  riinopn  16986  neiint  17173  topssnei  17193  restntr  17251  iscnp4  17332  cnconst2  17352  cnrest2  17355  cnprest2  17359  cnpdis  17362  cnt0  17415  cnt1  17419  cnhaus  17423  ordthauslem  17452  cncmp  17460  fiuncmp  17472  sscmp  17473  hauscmp  17475  cnconn  17490  uncon  17497  nlly2i  17544  llynlly  17545  nllyidm  17557  ptrescn  17676  xkococnlem  17696  qtoptop2  17736  qtopss  17752  kqfvima  17767  r0cld  17775  ordthmeolem  17838  fbssint  17875  fmf  17982  fmss  17983  elfm  17984  rnelfmlem  17989  rnelfm  17990  fmco  17998  flimss2  18009  flimss1  18010  flimrest  18020  flftg  18033  cnpflf2  18037  cnpflf  18038  flfcnp  18041  supnfcls  18057  fclsss1  18059  fclsss2  18060  fcfnei  18072  fcfelbas  18073  cnpfcfi  18077  subgntr  18141  opnsubg  18142  cldsubg  18145  ghmcnp  18149  utop2nei  18285  neipcfilu  18331  bldisj  18433  blgt0  18434  bl2in  18435  blss2ps  18438  blss2  18439  blssps  18459  blss  18460  xmetresbl  18472  lpbl  18538  blcld  18540  stdbdbl  18552  metcnp3  18575  metcnp2  18577  txmetcnp  18582  blval2  18610  nmoix  18768  nmoeq0  18775  icoopnst  18969  iocopnst  18970  xrhmeo  18976  nmhmcn  19133  cphsqrcl2  19154  cphsqrcl3  19155  cfil3i  19227  caublcls  19266  bcthlem5  19286  cmetcusp1OLD  19310  cmetcusp1  19311  pjth  19345  ovoliunlem2  19404  volun  19444  volsup2  19502  mbfimaopn2  19552  iblconst  19712  itgconst  19713  dvcnp2  19811  dvcn  19812  evlsval2  19946  deg1mul3le  20044  deg1tmle  20045  dvdsq1p  20088  ig1peu  20099  ig1pdvds  20104  coeid3  20164  dgrmulc  20194  efcvx  20370  tanord  20445  logdivlti  20520  logccv  20559  recxpcl  20571  cxpeq  20646  ang180  20661  isosctrlem2  20668  cxp2lim  20820  amgm  20834  muval1  20921  dvdssqf  20926  mumullem2  20968  mumul  20969  bcmono  21066  lgsfcl2  21091  lgsdilem  21111  lgsdirprm  21118  lgsdir  21119  lgsdi  21121  lgsne0  21122  2pthon  21607  gxcom  21862  gxnn0add  21867  zerdivemp1  22027  nvmul0or  22138  ipval2lem2  22205  ipval2lem5  22211  lnomul  22266  shless  22866  shlej1  22867  pjspansn  23084  hoadddi  23311  kbmul  23463  homco2  23485  kbass2  23625  snunioc  24142  eliccelico  24145  elicoelioo  24146  iocinioc2  24147  iocinif  24149  ress0g  24187  xrge0adddir  24220  xrge0npcan  24221  rhmdvdsr  24261  pstmfval  24296  fmcncfil  24322  zrhnm  24358  qqhnm  24379  measvunilem  24571  volfiniune  24591  dya2iocnrect  24636  probun  24682  probinc  24684  cndprob01  24698  pconpi1  24929  cvmsss2  24966  ntrivcvgmul  25235  binomrisefac  25363  dvdspw  25374  br6  25385  br4  25386  frrlem4  25590  brbtwn2  25849  colinearalglem1  25850  colinearalg  25854  axcgrtr  25859  axsegconlem8  25868  axsegconlem9  25869  axsegconlem10  25870  axcontlem8  25915  axcontlem10  25917  cgrcomim  25928  cgrtriv  25941  cgrextend  25947  segconeq  25949  btwntriv2  25951  btwnintr  25958  btwnexch3  25959  btwnouttr2  25961  trisegint  25967  cgrsub  25984  cgrxfr  25994  btwnxfr  25995  lineext  26015  btwnconn1lem13  26038  btwnconn1lem14  26039  btwnconn3  26042  segcon2  26044  brsegle  26047  brsegle2  26048  segletr  26053  segleantisym  26054  seglelin  26055  outsideofeu  26070  lineunray  26086  lineelsb2  26087  areacirc  26311  ivthALT  26352  finlocfin  26393  cocanfo  26433  upixp  26445  ismtyima  26526  rrndstprj2  26554  zerdivemp1x  26585  mzprename  26820  eldioph2lem1  26832  lzunuz  26840  rencldnfi  26896  pellexlem2  26907  infmrgelbi  26955  pellfundglb  26962  pellfund14gap  26964  qirropth  26985  rmxycomplete  26994  congadd  27045  acongeq  27062  jm2.19  27078  jm2.23  27081  jm2.20nn  27082  jm2.27  27093  jm3.1  27105  aomclem6  27148  lnmepi  27174  lmhmfgsplit  27175  lmhmlnmsplit  27176  pwssplit1  27179  pwssplit3  27181  pwssplit4  27182  uvcresum  27233  frlmsslsp  27239  frlmup4  27244  enfixsn  27248  lindff1  27281  f1lindf  27283  lsslindf  27291  islindf4  27299  lbslcic  27302  hbtlem2  27319  hbtlem5  27323  dgraa0p  27345  pmtrfb  27397  psgnunilem4  27411  mhmvlin  27443  hashgcdlem  27507  proot1hash  27510  stoweidlem19  27758  stoweidlem20  27759  stoweidlem22  27761  stoweidlem28  27767  stoweidlem34  27773  stoweidlem44  27783  stoweidlem60  27799  wallispilem3  27806  fzofzim  28159  fzoopth  28162  swrd0swrd  28231  swrdswrdlem  28232  swrdccatin12  28248  bnj517  29330  bnj594  29357  lubunNEW  29845  lsatfixedN  29881  lssat  29888  eqlkr  29971  eqlkr2  29972  lkrlsp  29974  lshpkrlem4  29985  opposet  30054  cvrcon3b  30149  cvrcmp  30155  atlen0  30182  atnle  30189  atlatmstc  30191  cvlatexch3  30210  cvlsupr2  30215  hlsupr2  30258  hlrelat2  30274  cvrexchlem  30290  lnnat  30298  atcvrj2b  30303  atle  30307  atexchcvrN  30311  atbtwn  30317  athgt  30327  3dimlem3  30332  3dim1  30338  1cvratlt  30345  1cvrjat  30346  ps-1  30348  ps-2  30349  3atlem3  30356  3atlem5  30358  3atlem7  30360  llni  30379  llni2  30383  atcvrlln2  30390  llnexatN  30392  llncmp  30393  2llnmat  30395  2at0mat0  30396  lplni  30403  lplnnle2at  30412  2atnelpln  30415  lplnllnneN  30427  llncvrlpln2  30428  2lplnmN  30430  2llnmj  30431  lplncmp  30433  lplnexatN  30434  lplnexllnN  30435  2llnm3N  30440  lvoli  30446  lvoli3  30448  islvol2aN  30463  4atlem0a  30464  4atlem3  30467  4atlem3a  30468  4atlem4a  30470  4atlem4b  30471  4atlem4c  30472  4atlem4d  30473  4atlem10b  30476  4atlem11  30480  4atlem12  30483  lplncvrlvol2  30486  lvolcmp  30488  2lplnmj  30493  islinei  30611  pmapglbx  30640  linepmap  30646  lneq2at  30649  lnjatN  30651  lncvrat  30653  lncmp  30654  2llnma3r  30659  elpaddatriN  30674  elpaddat  30675  paddcom  30684  paddss1  30688  paddss2  30689  paddss12  30690  paddasslem6  30696  paddasslem7  30697  paddasslem8  30698  paddasslem9  30699  paddasslem15  30705  pmodlem2  30718  pmodl42N  30722  pmapjoin  30723  llnmod1i2  30731  2polcon4bN  30789  polcon2bN  30791  poml4N  30824  poml6N  30826  osumcllem1N  30827  osumcllem2N  30828  osumcllem11N  30837  osumclN  30838  pmapojoinN  30839  pexmidlem2N  30842  pexmidlem3N  30843  pexmidlem4N  30844  pexmidlem6N  30846  pexmidlem7N  30847  pl42lem2N  30851  pl42lem3N  30852  pl42lem4N  30853  pl42N  30854  lhpexle2lem  30880  lhpexle3lem  30882  lhpexle3  30883  lhpmcvr3  30896  lhp2at0nle  30906  lhprelat3N  30911  4atex  30947  4atex2  30948  lauteq  30966  lautco  30968  ltrncoidN  30999  ltrneq2  31019  ltrnnidn  31045  ltrnideq  31046  trlnid  31050  ltrnatlw  31054  trlnle  31057  trlval3  31058  trlval4  31059  cdlemc  31068  cdlemd5  31073  cdlemd9  31077  ltrneq3  31079  cdleme0moN  31096  cdleme20  31195  cdleme21j  31207  cdleme21  31208  cdleme27cl  31237  cdlemefrs29bpre0  31267  cdlemefs27cl  31284  cdlemefs32sn1aw  31285  cdleme43fsv1snlem  31291  cdleme32d  31315  cdleme32f  31317  cdleme32le  31318  cdleme35h2  31328  cdleme38n  31335  cdleme40m  31338  cdleme41snaw  31347  cdleme42ke  31356  cdleme17d3  31367  cdleme48fvg  31371  cdlemeg46fvcl  31377  cdlemeg46fgN  31405  cdleme48gfv1  31407  cdleme48fgv  31409  cdleme50trn3  31424  trlord  31440  ltrniotavalbN  31455  cdlemb3  31477  cdlemg6c  31491  cdlemg6  31494  cdlemg7N  31497  cdlemg8c  31500  cdlemg8  31502  cdlemg11a  31508  cdlemg11b  31513  cdlemg12e  31518  cdlemg15a  31526  cdlemg15  31527  cdlemg16  31528  cdlemg16z  31530  cdlemg16zz  31531  cdlemg17dN  31534  cdlemg18a  31549  cdlemg20  31556  cdlemg22  31558  cdlemg24  31559  cdlemg37  31560  cdlemg31d  31571  cdlemg29  31576  cdlemg33b  31578  cdlemg33  31582  cdlemg38  31586  cdlemg39  31587  cdlemg40  31588  trlco  31598  trlcone  31599  cdlemg42  31600  cdlemg44b  31603  ltrncom  31609  trljco  31611  tendococl  31643  tendoplcl  31652  tendoplcom  31653  cdlemj2  31693  cdlemj3  31694  tendoid0  31696  tendoconid  31700  tendotr  31701  cdlemk25-3  31775  cdlemk26b-3  31776  cdlemk34  31781  cdlemk36  31784  cdlemk38  31786  cdlemkid4  31805  cdlemk35s-id  31809  cdlemk39s-id  31811  cdlemk19x  31814  cdlemk53  31828  cdlemk55  31832  cdlemk55u  31837  cdlemk39u  31839  cdlemk19u  31841  cdlemk56  31842  tendoex  31846  cdleml3N  31849  cdleml5N  31851  tendospcanN  31895  cdlemm10N  31990  cdlemn11pre  32082  dihord2pre  32097  dihvalcqpre  32107  dihopelvalcpre  32120  dihord6apre  32128  dihord5b  32131  dihord5apre  32134  dihord  32136  dihmeetlem1N  32162  dihglblem5apreN  32163  dihglblem3N  32167  dihmeetlem2N  32171  dihglbcpreN  32172  dihmeetbN  32175  dihmeetlem4preN  32178  dihmeetlem5  32180  dihmeetlem7N  32182  dihmeetlem10N  32188  dihmeetlem11N  32189  dihmeetlem12N  32190  dihmeetlem13N  32191  dihmeetlem15N  32193  dihmeetlem16N  32194  dihmeetlem17N  32195  dihmeetlem18N  32196  dihmeetlem19N  32197  dihmeetALTN  32199  dih1dimatlem0  32200  dihlspsnssN  32204  dihlspsnat  32205  mapdh8ad  32651  hdmap14lem14  32756  hgmapvvlem3  32800
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator