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

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

Proof of Theorem simpl3
StepHypRef Expression
1 simp3 959 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ch )
21adantr 452 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  simpll3  998  simprl3  1004  simp1l3  1052  simp2l3  1058  simp3l3  1064  3anandirs  1286  fcofo  5960  soisores  5986  weniso  6014  knatar  6019  smorndom  6566  nnmord  6811  nnmword  6812  difsnen  7126  mapunen  7212  ac6sfi  7287  fipreima  7347  wemaplem2  7449  en2eqpr  7824  indcardi  7855  acndom  7865  fodomfi2  7874  infmap2  8031  cflim2  8076  coftr  8086  infpssrlem4  8119  fin23lem11  8130  fincssdom  8136  isf32lem9  8174  fin1a2lem9  8221  gchpwdom  8482  gruima  8610  prpssnq  8800  distrlem4pr  8836  addcan  9182  addcan2  9183  ledivmul2OLD  9820  supmul1  9905  uzsupss  10500  xaddass  10760  xleadd1a  10764  xlesubadd  10774  xmulasslem3  10797  xadddilem  10805  xadddi  10806  ixxun  10864  icoshftf1o  10952  modsubdir  11212  ltexp2a  11358  leexp2  11361  ltexp2r  11363  exple1  11366  expnlbnd2  11437  hashtpg  11618  ccatass  11677  ccatopth  11703  s2f1o  11790  limsuplt  12200  limsupgre  12202  addcn2  12314  mulcn2  12316  dvdsmod  12833  gcdass  12972  rplpwr  12983  rppwr  12984  rpmulgcd2  13032  rpexp  13047  rpdvds  13051  prmdiveq  13102  coprimeprodsq  13110  coprimeprodsq2  13111  pythagtriplem3  13119  pcdvdsb  13169  pcgcd1  13177  pcbc  13196  0ram  13315  ramz2  13319  ramub1lem1  13321  mremre  13756  mrieqv2d  13791  lubun  14477  issubmnd  14651  gsumccat  14714  frmdss2  14735  mulgnn0p1  14828  mulgnnsubcl  14829  mulgneg  14835  mulgdirlem  14841  nmzsubg  14908  ghmmulg  14945  odmodnn0  15105  oddvdsnn0  15109  odnncl  15110  odmod  15111  oddvds  15112  odeq  15115  odmulgid  15117  odmulg  15119  odmulgeq  15120  odbezout  15121  odf1o1  15133  odf1o2  15134  odngen  15138  odcau  15165  pgpssslw  15175  fislw  15186  lsmless1x  15205  lsmless2x  15206  lsmsubm  15214  lsmmod  15234  lsmmod2  15235  efgsfo  15298  cntzcmn  15386  odadd1  15390  odadd2  15391  odadd  15392  lsmcomx  15398  prdscmnd  15403  gsumconst  15459  rng1eq0  15629  cntzsubr  15827  isabvd  15835  lspss  15987  0lmhm  16043  reslmhm2  16056  lbspss  16081  lspfixed  16127  lsmcv  16140  lspsnat  16144  issubassa  16310  aspss  16318  coe1subfv  16586  coe1tm  16592  xrsdsreclblem  16667  obselocv  16878  neiint  17091  topssnei  17111  cnrest2  17272  cnprest2  17276  cnt0  17332  cnt1  17336  cnhaus  17340  cncmp  17377  fiuncmp  17389  sscmp  17390  hauscmp  17392  cnconn  17406  uncon  17413  kgen2ss  17508  ptpjopn  17565  ptrescn  17592  qtopss  17668  kqfvima  17683  r0cld  17691  cmphaushmeo  17753  fbssint  17791  fbasrn  17837  filuni  17838  ufilmax  17860  fin1aufil  17885  fmf  17898  fmss  17899  rnelfmlem  17905  rnelfm  17906  fmufil  17912  fmco  17914  flimss2  17925  flimss1  17926  flimrest  17936  cnpflf2  17953  cnpflf  17954  flfcnp  17957  lmflf  17958  supnfcls  17973  fclsss1  17975  fclsss2  17976  cnpfcfi  17993  subgntr  18057  opnsubg  18058  cldsubg  18061  ustuqtop1  18192  ucncn  18236  bldisj  18329  blgt0  18330  bl2in  18331  blss2  18333  xbln0  18339  blss  18346  lpbl  18423  blcld  18425  blcls  18426  stdbdmopn  18438  metcnp2  18462  txmetcnp  18467  blval2  18482  restmetu  18489  nmoix  18634  nmoi2  18635  nmoeq0  18641  nmotri  18644  metdsge  18750  metds0  18751  metdseq0  18755  icoopnst  18835  iccpnfhmeo  18841  xrhmeo  18842  nmhmcn  18999  cphsqrcl2  19020  cphsqrcl3  19021  fmcfil  19096  bcthlem5  19150  cmetcusp1  19174  pjth  19207  ovolunnul  19263  volun  19306  voliunlem2  19312  itg2const  19499  iblconst  19576  itgconst  19577  limcvallem  19625  dvcnp2  19673  dvcn  19674  deg1mul3le  19906  deg1tmle  19907  ig1pdvds  19966  coe11  20038  dgrmulc  20056  dvply1  20068  aaliou2  20124  efcvx  20232  tanord  20307  logdivlti  20382  logccv  20421  recxpcl  20433  cxplea  20454  cxple2a  20457  ang180  20523  isosctrlem2  20530  cxp2lim  20682  amgm  20696  muval1  20783  dvdssqf  20788  mumullem2  20830  bcmono  20928  lgsneg  20970  lgsmod  20972  lgsdirprm  20980  lgsdir  20981  lgsdi  20983  cyclispthon  21468  vdgrfif  21518  zerdivemp1  21870  nvmul0or  21981  shless  22709  shlej1  22710  pjspansn  22927  kbmul  23306  homco2  23328  kbass2  23468  snunioc  23973  eliccelico  23976  elicoelioo  23977  iocinioc2  23978  difioo  23981  xrge0npcan  24045  fmcncfil  24121  zrhnm  24154  qqhnm  24173  volfiniune  24380  probinc  24458  cndprob01  24472  cvmsss2  24740  dedekind  24966  dvdspw  25127  funsseq  25149  sltres  25342  brbtwn2  25558  colinearalglem1  25559  colinearalg  25563  axcgrtr  25568  axcontlem2  25618  cgrtriv  25650  5segofs  25654  btwntriv2  25660  btwnxfr  25704  segcon2  25753  brsegle2  25757  seglelin  25764  outsideofeu  25779  bpolydif  25815  comppfsc  26078  blbnd  26187  rrndstprj2  26231  zerdivemp1x  26262  ofmpteq  26467  mzpsubst  26496  diophrw  26508  eldioph2lem1  26509  rencldnfi  26573  pellexlem2  26584  pellqrexplicit  26631  infmrgelbi  26632  rmxycomplete  26671  congadd  26722  acongeq  26739  jm2.19  26755  jm2.22  26757  jm2.20nn  26759  jm2.25lem1  26760  jm2.27  26770  jm3.1  26782  lmhmlnmsplit  26854  pwssplit0  26856  pwssplit1  26857  pwssplit4  26860  frlmsplit2  26912  frlmsslss2  26914  frlmup4  26922  lindff1  26959  lsslindf  26969  lsslinds  26970  islindf4  26977  hbtlem2  26997  dgraa0p  27023  pmtrfv  27064  pmtrmvd  27067  pmtrfb  27075  idomrootle  27180  hashgcdlem  27185  proot1hash  27188  fmul01  27378  ibliccsinexp  27413  iblioosinexp  27415  stoweidlem20  27437  stoweidlem22  27439  stoweidlem34  27451  stoweidlem44  27461  stoweidlem60  27477  wallispilem3  27484  4cyclusnfrgra  27772  lubunNEW  29088  lsmsat  29123  lsatfixedN  29124  lssat  29131  lkrlsp  29217  lshpkrlem4  29228  op1cl  29300  cvrcon3b  29392  leat3  29410  atlen0  29425  atnle  29432  atlatmstc  29434  atlatle  29435  cvlcvr1  29454  cvlsupr2  29458  hlsupr2  29501  hlrelat2  29517  cvrexchlem  29533  cvratlem  29535  lnnat  29541  atexchcvrN  29554  1cvratlt  29588  1cvrjat  29589  3atlem3  29599  3atlem7  29603  llni2  29626  atcvrlln2  29633  llnexatN  29635  llncmp  29636  2llnmat  29638  2at0mat0  29639  2atnelpln  29658  llncvrlpln2  29671  2lplnmN  29673  2llnmj  29674  lplncmp  29676  lplnexatN  29677  2llnjaN  29680  lvoli3  29691  islvol2aN  29706  4atlem3a  29711  4atlem4a  29713  4atlem4b  29714  4atlem11  29723  4atlem12  29726  lplncvrlvol2  29729  lvolcmp  29731  2lplnmj  29736  islinei  29854  linepmap  29889  lneq2at  29892  2llnma3r  29902  elpaddn0  29914  elpaddatriN  29917  elpaddat  29918  paddcom  29927  paddss1  29931  paddss2  29932  paddasslem6  29939  paddasslem7  29940  paddasslem10  29943  paddasslem15  29948  pmodlem2  29961  pmodl42N  29965  pmapjoin  29966  atmod1i1m  29972  llnmod1i2  29974  llnexchb2lem  29982  polcon2bN  30034  pclfinclN  30064  poml4N  30067  poml6N  30069  osumcllem11N  30080  osumclN  30081  pmapojoinN  30082  pexmidlem2N  30085  pexmidlem3N  30086  pexmidlem4N  30087  pexmidlem6N  30089  pexmidlem7N  30090  pl42lem2N  30094  pl42lem3N  30095  pl42lem4N  30096  pl42N  30097  lhpexle3lem  30125  lhpmcvr3  30139  lhp2at0nle  30149  lhprelat3N  30154  lauteq  30209  lautco  30211  ltrncoidN  30242  ltrneq2  30262  ltrnnidn  30288  ltrnideq  30289  trlnle  30300  cdlemc  30311  cdlemd4  30315  cdlemd5  30316  cdlemd9  30320  cdlemd  30321  ltrneq3  30322  cdlemefrs29pre00  30509  cdlemefrs29cpre1  30512  cdlemefrs29clN  30513  cdlemefrs32fva  30514  cdlemefr29exN  30516  cdlemefr27cl  30517  cdlemefs27cl  30527  cdlemefs32sn1aw  30528  cdleme32fva  30551  cdleme32d  30558  cdleme32f  30560  cdleme32le  30561  cdleme40n  30582  cdleme41snaw  30590  cdleme17d3  30610  cdleme48fvg  30614  cdlemeg46fvcl  30620  cdlemeg46fgN  30648  cdleme48fgv  30652  ltrniotavalbN  30698  cdlemb3  30720  cdlemg15  30770  cdlemg17dN  30777  trlco  30841  cdlemg44b  30846  ltrncom  30852  trljco  30854  tendococl  30886  tendoplcl  30895  tendoplcom  30896  tendotr  30944  cdlemk36  31027  cdlemk35s-id  31052  cdlemk39s-id  31054  cdlemk19x  31057  cdlemk53b  31070  cdlemk55  31075  cdlemk35u  31078  cdlemk55u  31080  cdlemk39u  31082  cdlemk19u  31084  cdlemk56  31085  tendoex  31089  cdleml5N  31094  dihord2pre  31340  dihord6apre  31371  dihord5b  31374  dihord5apre  31377  dihord  31379  dihmeetlem1N  31405  dihmeetlem2N  31414  dihglbcpreN  31415  dihmeetbN  31418  dihmeetlem4preN  31421  dihmeetlem5  31423  dihmeetlem6  31424  dihmeetlem7N  31425  dihmeetlem10N  31431  dihmeetlem11N  31432  dihmeetlem12N  31433  dihmeetlem13N  31434  dihmeetlem15N  31436  dihmeetlem17N  31438  dihmeetlem18N  31439  dihmeetlem19N  31440  dihmeetALTN  31442  dih1dimatlem0  31443  dihlspsnssN  31447  dvh3dim2  31563
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