MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simpl1 Structured version   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  3054  brcogw  5033  cocan1  6016  weniso  6067  smogt  6621  smorndom  6622  omeulem1  6817  nnmord  6867  nnmword  6868  difsnen  7182  mapunen  7268  ac6sfi  7343  fipreima  7404  elfiun  7427  ordiso2  7476  wemaplem2  7508  wemapso  7512  en2eqpr  7883  indcardi  7914  fodomfi2  7933  iunfictbso  7987  infmap2  8090  cofsmo  8141  cfsmolem  8142  coftr  8145  fin23lem11  8189  fincssdom  8195  fin23lem26  8197  isf32lem9  8233  ac6num  8351  gchdomtri  8496  gchpwdom  8541  winainflem  8560  tskuni  8650  gruima  8669  gruf  8678  grudomon  8684  elnpi  8857  distrlem4pr  8895  prlem934  8902  addcan  9242  addcan2  9243  ltmul1a  9851  ledivmulOLD  9876  ledivmul2OLD  9880  suprleub  9964  supmul1  9965  infmrgelb  9980  suprzcl  10341  uzsupss  10560  xleadd1a  10824  xlesubadd  10834  xmulasslem3  10857  xlemul2a  10860  xadddilem  10865  xadddi2  10868  ixxun  10924  icoshftf1o  11012  lincmb01cmp  11030  iccf1o  11031  ltexp2a  11423  leexp2  11426  ltexp2r  11428  exple1  11431  expnlbnd2  11502  ccatass  11742  ccatopth  11768  s2f1o  11855  limsupgre  12267  addcn2  12379  mulcn2  12381  dvdsadd2b  12884  dvdsmod  12898  oexpneg  12903  gcdass  13037  rplpwr  13048  rppwr  13049  coprmdvds2  13095  rpmulgcd2  13097  qredeq  13098  rpexp  13112  rpdvds  13116  prmdiveq  13167  odzdvds  13173  coprimeprodsq2  13176  pythagtriplem3  13184  pcdvdsb  13234  pcgcd1  13242  qexpz  13262  pockthg  13266  vdwnnlem1  13355  0ram  13380  ramz2  13384  lubss  14540  lubun  14542  clatleglb  14545  clatglbss  14546  mrelatglb  14602  issubmnd  14716  gsumccat  14779  frmdss2  14800  mulgneg  14900  mulgdirlem  14906  submmulg  14917  subgmulg  14950  nmzsubg  14973  ghmmulg  15010  odmodnn0  15170  odnncl  15175  odmod  15176  odmulgid  15182  odmulgeq  15185  odf1o1  15198  odf1o2  15199  odngen  15203  gexdvdsi  15209  pgpfi1  15221  odcau  15230  subgslw  15242  fislw  15251  lsmssv  15269  lsmless1x  15270  lsmless2x  15271  lsmsubm  15279  lsmmod  15299  lsmmod2  15300  efgred  15372  cntzcmn  15451  ghmplusg  15453  odadd1  15455  odadd2  15456  odadd  15457  lsmcomx  15463  gsumconst  15524  rng1eq0  15694  mulgass2  15702  isabvd  15900  lssintcl  16032  0lmhm  16108  lmhmvsca  16113  reslmhm2b  16122  lspfixed  16192  lspsnat  16209  lidldvgen  16318  issubassa  16375  psrplusgpropd  16621  coe1subfv  16651  coe1mul2  16654  xrsdsreclblem  16736  obselocv  16947  riinopn  16973  neiint  17160  topssnei  17180  restntr  17238  iscnp4  17319  cnconst2  17339  cnrest2  17342  cnprest2  17346  cnpdis  17349  cnt0  17402  cnt1  17406  cnhaus  17410  ordthauslem  17439  cncmp  17447  fiuncmp  17459  sscmp  17460  hauscmp  17462  cnconn  17477  uncon  17484  nlly2i  17531  llynlly  17532  nllyidm  17544  ptrescn  17663  xkococnlem  17683  qtoptop2  17723  qtopss  17739  kqfvima  17754  r0cld  17762  ordthmeolem  17825  fbssint  17862  fmf  17969  fmss  17970  elfm  17971  rnelfmlem  17976  rnelfm  17977  fmco  17985  flimss2  17996  flimss1  17997  flimrest  18007  flftg  18020  cnpflf2  18024  cnpflf  18025  flfcnp  18028  supnfcls  18044  fclsss1  18046  fclsss2  18047  fcfnei  18059  fcfelbas  18060  cnpfcfi  18064  subgntr  18128  opnsubg  18129  cldsubg  18132  ghmcnp  18136  utop2nei  18272  neipcfilu  18318  bldisj  18420  blgt0  18421  bl2in  18422  blss2ps  18425  blss2  18426  blssps  18446  blss  18447  xmetresbl  18459  lpbl  18525  blcld  18527  stdbdbl  18539  metcnp3  18562  metcnp2  18564  txmetcnp  18569  blval2  18597  nmoix  18755  nmoeq0  18762  icoopnst  18956  iocopnst  18957  xrhmeo  18963  nmhmcn  19120  cphsqrcl2  19141  cphsqrcl3  19142  cfil3i  19214  caublcls  19253  bcthlem5  19273  cmetcusp1OLD  19297  cmetcusp1  19298  pjth  19332  ovoliunlem2  19391  volun  19431  volsup2  19489  mbfimaopn2  19541  iblconst  19701  itgconst  19702  dvcnp2  19798  dvcn  19799  evlsval2  19933  deg1mul3le  20031  deg1tmle  20032  dvdsq1p  20075  ig1peu  20086  ig1pdvds  20091  coeid3  20151  dgrmulc  20181  efcvx  20357  tanord  20432  logdivlti  20507  logccv  20546  recxpcl  20558  cxpeq  20633  ang180  20648  isosctrlem2  20655  cxp2lim  20807  amgm  20821  muval1  20908  dvdssqf  20913  mumullem2  20955  mumul  20956  bcmono  21053  lgsfcl2  21078  lgsdilem  21098  lgsdirprm  21105  lgsdir  21106  lgsdi  21108  lgsne0  21109  2pthon  21594  gxcom  21849  gxnn0add  21854  zerdivemp1  22014  nvmul0or  22125  ipval2lem2  22192  ipval2lem5  22198  lnomul  22253  shless  22853  shlej1  22854  pjspansn  23071  hoadddi  23298  kbmul  23450  homco2  23472  kbass2  23612  snunioc  24129  eliccelico  24132  elicoelioo  24133  iocinioc2  24134  iocinif  24136  ress0g  24174  xrge0adddir  24207  xrge0npcan  24208  rhmdvdsr  24248  pstmfval  24283  fmcncfil  24309  zrhnm  24345  qqhnm  24366  measvunilem  24558  volfiniune  24578  dya2iocnrect  24623  probun  24669  probinc  24671  cndprob01  24685  pconpi1  24916  cvmsss2  24953  ntrivcvgmul  25222  binomrisefac  25350  dvdspw  25361  br6  25372  br4  25373  frrlem4  25577  brbtwn2  25836  colinearalglem1  25837  colinearalg  25841  axcgrtr  25846  axsegconlem8  25855  axsegconlem9  25856  axsegconlem10  25857  axcontlem8  25902  axcontlem10  25904  cgrcomim  25915  cgrtriv  25928  cgrextend  25934  segconeq  25936  btwntriv2  25938  btwnintr  25945  btwnexch3  25946  btwnouttr2  25948  trisegint  25954  cgrsub  25971  cgrxfr  25981  btwnxfr  25982  lineext  26002  btwnconn1lem13  26025  btwnconn1lem14  26026  btwnconn3  26029  segcon2  26031  brsegle  26034  brsegle2  26035  segletr  26040  segleantisym  26041  seglelin  26042  outsideofeu  26057  lineunray  26073  lineelsb2  26074  areacirc  26288  ivthALT  26329  finlocfin  26370  cocanfo  26410  upixp  26422  ismtyima  26503  rrndstprj2  26531  zerdivemp1x  26562  mzprename  26797  eldioph2lem1  26809  lzunuz  26817  rencldnfi  26873  pellexlem2  26884  infmrgelbi  26932  pellfundglb  26939  pellfund14gap  26941  qirropth  26962  rmxycomplete  26971  congadd  27022  acongeq  27039  jm2.19  27055  jm2.23  27058  jm2.20nn  27059  jm2.27  27070  jm3.1  27082  aomclem6  27125  lnmepi  27151  lmhmfgsplit  27152  lmhmlnmsplit  27153  pwssplit1  27156  pwssplit3  27158  pwssplit4  27159  uvcresum  27210  frlmsslsp  27216  frlmup4  27221  enfixsn  27225  lindff1  27258  f1lindf  27260  lsslindf  27268  islindf4  27276  lbslcic  27279  hbtlem2  27296  hbtlem5  27300  dgraa0p  27322  pmtrfb  27374  psgnunilem4  27388  mhmvlin  27420  hashgcdlem  27484  proot1hash  27487  stoweidlem19  27735  stoweidlem20  27736  stoweidlem22  27738  stoweidlem28  27744  stoweidlem34  27750  stoweidlem44  27760  stoweidlem60  27776  wallispilem3  27783  swrd0swrd  28163  swrdswrdlem  28164  swrdccatin12  28180  bnj517  29193  bnj594  29220  lubunNEW  29708  lsatfixedN  29744  lssat  29751  eqlkr  29834  eqlkr2  29835  lkrlsp  29837  lshpkrlem4  29848  opposet  29917  cvrcon3b  30012  cvrcmp  30018  atlen0  30045  atnle  30052  atlatmstc  30054  cvlatexch3  30073  cvlsupr2  30078  hlsupr2  30121  hlrelat2  30137  cvrexchlem  30153  lnnat  30161  atcvrj2b  30166  atle  30170  atexchcvrN  30174  atbtwn  30180  athgt  30190  3dimlem3  30195  3dim1  30201  1cvratlt  30208  1cvrjat  30209  ps-1  30211  ps-2  30212  3atlem3  30219  3atlem5  30221  3atlem7  30223  llni  30242  llni2  30246  atcvrlln2  30253  llnexatN  30255  llncmp  30256  2llnmat  30258  2at0mat0  30259  lplni  30266  lplnnle2at  30275  2atnelpln  30278  lplnllnneN  30290  llncvrlpln2  30291  2lplnmN  30293  2llnmj  30294  lplncmp  30296  lplnexatN  30297  lplnexllnN  30298  2llnm3N  30303  lvoli  30309  lvoli3  30311  islvol2aN  30326  4atlem0a  30327  4atlem3  30330  4atlem3a  30331  4atlem4a  30333  4atlem4b  30334  4atlem4c  30335  4atlem4d  30336  4atlem10b  30339  4atlem11  30343  4atlem12  30346  lplncvrlvol2  30349  lvolcmp  30351  2lplnmj  30356  islinei  30474  pmapglbx  30503  linepmap  30509  lneq2at  30512  lnjatN  30514  lncvrat  30516  lncmp  30517  2llnma3r  30522  elpaddatriN  30537  elpaddat  30538  paddcom  30547  paddss1  30551  paddss2  30552  paddss12  30553  paddasslem6  30559  paddasslem7  30560  paddasslem8  30561  paddasslem9  30562  paddasslem15  30568  pmodlem2  30581  pmodl42N  30585  pmapjoin  30586  llnmod1i2  30594  2polcon4bN  30652  polcon2bN  30654  poml4N  30687  poml6N  30689  osumcllem1N  30690  osumcllem2N  30691  osumcllem11N  30700  osumclN  30701  pmapojoinN  30702  pexmidlem2N  30705  pexmidlem3N  30706  pexmidlem4N  30707  pexmidlem6N  30709  pexmidlem7N  30710  pl42lem2N  30714  pl42lem3N  30715  pl42lem4N  30716  pl42N  30717  lhpexle2lem  30743  lhpexle3lem  30745  lhpexle3  30746  lhpmcvr3  30759  lhp2at0nle  30769  lhprelat3N  30774  4atex  30810  4atex2  30811  lauteq  30829  lautco  30831  ltrncoidN  30862  ltrneq2  30882  ltrnnidn  30908  ltrnideq  30909  trlnid  30913  ltrnatlw  30917  trlnle  30920  trlval3  30921  trlval4  30922  cdlemc  30931  cdlemd5  30936  cdlemd9  30940  ltrneq3  30942  cdleme0moN  30959  cdleme20  31058  cdleme21j  31070  cdleme21  31071  cdleme27cl  31100  cdlemefrs29bpre0  31130  cdlemefs27cl  31147  cdlemefs32sn1aw  31148  cdleme43fsv1snlem  31154  cdleme32d  31178  cdleme32f  31180  cdleme32le  31181  cdleme35h2  31191  cdleme38n  31198  cdleme40m  31201  cdleme41snaw  31210  cdleme42ke  31219  cdleme17d3  31230  cdleme48fvg  31234  cdlemeg46fvcl  31240  cdlemeg46fgN  31268  cdleme48gfv1  31270  cdleme48fgv  31272  cdleme50trn3  31287  trlord  31303  ltrniotavalbN  31318  cdlemb3  31340  cdlemg6c  31354  cdlemg6  31357  cdlemg7N  31360  cdlemg8c  31363  cdlemg8  31365  cdlemg11a  31371  cdlemg11b  31376  cdlemg12e  31381  cdlemg15a  31389  cdlemg15  31390  cdlemg16  31391  cdlemg16z  31393  cdlemg16zz  31394  cdlemg17dN  31397  cdlemg18a  31412  cdlemg20  31419  cdlemg22  31421  cdlemg24  31422  cdlemg37  31423  cdlemg31d  31434  cdlemg29  31439  cdlemg33b  31441  cdlemg33  31445  cdlemg38  31449  cdlemg39  31450  cdlemg40  31451  trlco  31461  trlcone  31462  cdlemg42  31463  cdlemg44b  31466  ltrncom  31472  trljco  31474  tendococl  31506  tendoplcl  31515  tendoplcom  31516  cdlemj2  31556  cdlemj3  31557  tendoid0  31559  tendoconid  31563  tendotr  31564  cdlemk25-3  31638  cdlemk26b-3  31639  cdlemk34  31644  cdlemk36  31647  cdlemk38  31649  cdlemkid4  31668  cdlemk35s-id  31672  cdlemk39s-id  31674  cdlemk19x  31677  cdlemk53  31691  cdlemk55  31695  cdlemk55u  31700  cdlemk39u  31702  cdlemk19u  31704  cdlemk56  31705  tendoex  31709  cdleml3N  31712  cdleml5N  31714  tendospcanN  31758  cdlemm10N  31853  cdlemn11pre  31945  dihord2pre  31960  dihvalcqpre  31970  dihopelvalcpre  31983  dihord6apre  31991  dihord5b  31994  dihord5apre  31997  dihord  31999  dihmeetlem1N  32025  dihglblem5apreN  32026  dihglblem3N  32030  dihmeetlem2N  32034  dihglbcpreN  32035  dihmeetbN  32038  dihmeetlem4preN  32041  dihmeetlem5  32043  dihmeetlem7N  32045  dihmeetlem10N  32051  dihmeetlem11N  32052  dihmeetlem12N  32053  dihmeetlem13N  32054  dihmeetlem15N  32056  dihmeetlem16N  32057  dihmeetlem17N  32058  dihmeetlem18N  32059  dihmeetlem19N  32060  dihmeetALTN  32062  dih1dimatlem0  32063  dihlspsnssN  32067  dihlspsnat  32068  mapdh8ad  32514  hdmap14lem14  32619  hgmapvvlem3  32663
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