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  5980  soisores  6006  weniso  6034  knatar  6039  smorndom  6589  nnmord  6834  nnmword  6835  difsnen  7149  mapunen  7235  ac6sfi  7310  fipreima  7370  wemaplem2  7472  en2eqpr  7847  indcardi  7878  acndom  7888  fodomfi2  7897  infmap2  8054  cflim2  8099  coftr  8109  infpssrlem4  8142  fin23lem11  8153  fincssdom  8159  isf32lem9  8197  fin1a2lem9  8244  gchpwdom  8505  gruima  8633  prpssnq  8823  distrlem4pr  8859  addcan  9206  addcan2  9207  ledivmul2OLD  9844  supmul1  9929  uzsupss  10524  xaddass  10784  xleadd1a  10788  xlesubadd  10798  xmulasslem3  10821  xadddilem  10829  xadddi  10830  ixxun  10888  icoshftf1o  10976  modsubdir  11240  ltexp2a  11386  leexp2  11389  ltexp2r  11391  exple1  11394  expnlbnd2  11465  hashtpg  11646  ccatass  11705  ccatopth  11731  s2f1o  11818  limsuplt  12228  limsupgre  12230  addcn2  12342  mulcn2  12344  dvdsmod  12861  gcdass  13000  rplpwr  13011  rppwr  13012  rpmulgcd2  13060  rpexp  13075  rpdvds  13079  prmdiveq  13130  coprimeprodsq  13138  coprimeprodsq2  13139  pythagtriplem3  13147  pcdvdsb  13197  pcgcd1  13205  pcbc  13224  0ram  13343  ramz2  13347  ramub1lem1  13349  mremre  13784  mrieqv2d  13819  lubun  14505  issubmnd  14679  gsumccat  14742  frmdss2  14763  mulgnn0p1  14856  mulgnnsubcl  14857  mulgneg  14863  mulgdirlem  14869  nmzsubg  14936  ghmmulg  14973  odmodnn0  15133  oddvdsnn0  15137  odnncl  15138  odmod  15139  oddvds  15140  odeq  15143  odmulgid  15145  odmulg  15147  odmulgeq  15148  odbezout  15149  odf1o1  15161  odf1o2  15162  odngen  15166  odcau  15193  pgpssslw  15203  fislw  15214  lsmless1x  15233  lsmless2x  15234  lsmsubm  15242  lsmmod  15262  lsmmod2  15263  efgsfo  15326  cntzcmn  15414  odadd1  15418  odadd2  15419  odadd  15420  lsmcomx  15426  prdscmnd  15431  gsumconst  15487  rng1eq0  15657  cntzsubr  15855  isabvd  15863  lspss  16015  0lmhm  16071  reslmhm2  16084  lbspss  16109  lspfixed  16155  lsmcv  16168  lspsnat  16172  issubassa  16338  aspss  16346  coe1subfv  16614  coe1tm  16620  xrsdsreclblem  16699  obselocv  16910  neiint  17123  topssnei  17143  cnrest2  17304  cnprest2  17308  cnt0  17364  cnt1  17368  cnhaus  17372  cncmp  17409  fiuncmp  17421  sscmp  17422  hauscmp  17424  cnconn  17438  uncon  17445  kgen2ss  17540  ptpjopn  17597  ptrescn  17624  qtopss  17700  kqfvima  17715  r0cld  17723  cmphaushmeo  17785  fbssint  17823  fbasrn  17869  filuni  17870  ufilmax  17892  fin1aufil  17917  fmf  17930  fmss  17931  rnelfmlem  17937  rnelfm  17938  fmufil  17944  fmco  17946  flimss2  17957  flimss1  17958  flimrest  17968  cnpflf2  17985  cnpflf  17986  flfcnp  17989  lmflf  17990  supnfcls  18005  fclsss1  18007  fclsss2  18008  cnpfcfi  18025  subgntr  18089  opnsubg  18090  cldsubg  18093  ustuqtop1  18224  ucncn  18268  bldisj  18381  blgt0  18382  bl2in  18383  blss2ps  18386  blss2  18387  xbln0  18397  blssps  18407  blss  18408  lpbl  18486  blcld  18488  blcls  18489  stdbdmopn  18501  metcnp2  18525  txmetcnp  18530  blval2  18558  restmetu  18570  nmoix  18716  nmoi2  18717  nmoeq0  18723  nmotri  18726  metdsge  18832  metds0  18833  metdseq0  18837  icoopnst  18917  iccpnfhmeo  18923  xrhmeo  18924  nmhmcn  19081  cphsqrcl2  19102  cphsqrcl3  19103  fmcfil  19178  bcthlem5  19234  cmetcusp1OLD  19258  cmetcusp1  19259  pjth  19293  ovolunnul  19349  volun  19392  voliunlem2  19398  itg2const  19585  iblconst  19662  itgconst  19663  limcvallem  19711  dvcnp2  19759  dvcn  19760  deg1mul3le  19992  deg1tmle  19993  ig1pdvds  20052  coe11  20124  dgrmulc  20142  dvply1  20154  aaliou2  20210  efcvx  20318  tanord  20393  logdivlti  20468  logccv  20507  recxpcl  20519  cxplea  20540  cxple2a  20543  ang180  20609  isosctrlem2  20616  cxp2lim  20768  amgm  20782  muval1  20869  dvdssqf  20874  mumullem2  20916  bcmono  21014  lgsneg  21056  lgsmod  21058  lgsdirprm  21066  lgsdir  21067  lgsdi  21069  cyclispthon  21573  vdgrfif  21623  zerdivemp1  21975  nvmul0or  22086  shless  22814  shlej1  22815  pjspansn  23032  kbmul  23411  homco2  23433  kbass2  23573  snunioc  24090  eliccelico  24093  elicoelioo  24094  iocinioc2  24095  difioo  24098  xrge0npcan  24169  isarchi2  24208  pstmfval  24244  fmcncfil  24270  zrhnm  24306  qqhnm  24327  volfiniune  24539  probinc  24632  cndprob01  24646  cvmsss2  24914  dedekind  25140  binomrisefac  25309  dvdspw  25317  funsseq  25339  sltres  25532  brbtwn2  25748  colinearalglem1  25749  colinearalg  25753  axcgrtr  25758  axcontlem2  25808  cgrtriv  25840  5segofs  25844  btwntriv2  25850  btwnxfr  25894  segcon2  25943  brsegle2  25947  seglelin  25954  outsideofeu  25969  bpolydif  26005  mblfinlem  26143  comppfsc  26277  blbnd  26386  rrndstprj2  26430  zerdivemp1x  26461  ofmpteq  26666  mzpsubst  26695  diophrw  26707  eldioph2lem1  26708  rencldnfi  26772  pellexlem2  26783  pellqrexplicit  26830  infmrgelbi  26831  rmxycomplete  26870  congadd  26921  acongeq  26938  jm2.19  26954  jm2.22  26956  jm2.20nn  26958  jm2.25lem1  26959  jm2.27  26969  jm3.1  26981  lmhmlnmsplit  27053  pwssplit0  27055  pwssplit1  27056  pwssplit4  27059  frlmsplit2  27111  frlmsslss2  27113  frlmup4  27121  lindff1  27158  lsslindf  27168  lsslinds  27169  islindf4  27176  hbtlem2  27196  dgraa0p  27222  pmtrfv  27263  pmtrmvd  27266  pmtrfb  27274  idomrootle  27379  hashgcdlem  27384  proot1hash  27387  fmul01  27577  ibliccsinexp  27612  iblioosinexp  27614  stoweidlem20  27636  stoweidlem22  27638  stoweidlem34  27650  stoweidlem44  27660  stoweidlem60  27676  wallispilem3  27683  fzo1fzo0n0  27988  swrdnd  28001  swrdccatin2  28018  swrdccatin12lem3a  28021  4cyclusnfrgra  28123  lubunNEW  29456  lsmsat  29491  lsatfixedN  29492  lssat  29499  lkrlsp  29585  lshpkrlem4  29596  op1cl  29668  cvrcon3b  29760  leat3  29778  atlen0  29793  atnle  29800  atlatmstc  29802  atlatle  29803  cvlcvr1  29822  cvlsupr2  29826  hlsupr2  29869  hlrelat2  29885  cvrexchlem  29901  cvratlem  29903  lnnat  29909  atexchcvrN  29922  1cvratlt  29956  1cvrjat  29957  3atlem3  29967  3atlem7  29971  llni2  29994  atcvrlln2  30001  llnexatN  30003  llncmp  30004  2llnmat  30006  2at0mat0  30007  2atnelpln  30026  llncvrlpln2  30039  2lplnmN  30041  2llnmj  30042  lplncmp  30044  lplnexatN  30045  2llnjaN  30048  lvoli3  30059  islvol2aN  30074  4atlem3a  30079  4atlem4a  30081  4atlem4b  30082  4atlem11  30091  4atlem12  30094  lplncvrlvol2  30097  lvolcmp  30099  2lplnmj  30104  islinei  30222  linepmap  30257  lneq2at  30260  2llnma3r  30270  elpaddn0  30282  elpaddatriN  30285  elpaddat  30286  paddcom  30295  paddss1  30299  paddss2  30300  paddasslem6  30307  paddasslem7  30308  paddasslem10  30311  paddasslem15  30316  pmodlem2  30329  pmodl42N  30333  pmapjoin  30334  atmod1i1m  30340  llnmod1i2  30342  llnexchb2lem  30350  polcon2bN  30402  pclfinclN  30432  poml4N  30435  poml6N  30437  osumcllem11N  30448  osumclN  30449  pmapojoinN  30450  pexmidlem2N  30453  pexmidlem3N  30454  pexmidlem4N  30455  pexmidlem6N  30457  pexmidlem7N  30458  pl42lem2N  30462  pl42lem3N  30463  pl42lem4N  30464  pl42N  30465  lhpexle3lem  30493  lhpmcvr3  30507  lhp2at0nle  30517  lhprelat3N  30522  lauteq  30577  lautco  30579  ltrncoidN  30610  ltrneq2  30630  ltrnnidn  30656  ltrnideq  30657  trlnle  30668  cdlemc  30679  cdlemd4  30683  cdlemd5  30684  cdlemd9  30688  cdlemd  30689  ltrneq3  30690  cdlemefrs29pre00  30877  cdlemefrs29cpre1  30880  cdlemefrs29clN  30881  cdlemefrs32fva  30882  cdlemefr29exN  30884  cdlemefr27cl  30885  cdlemefs27cl  30895  cdlemefs32sn1aw  30896  cdleme32fva  30919  cdleme32d  30926  cdleme32f  30928  cdleme32le  30929  cdleme40n  30950  cdleme41snaw  30958  cdleme17d3  30978  cdleme48fvg  30982  cdlemeg46fvcl  30988  cdlemeg46fgN  31016  cdleme48fgv  31020  ltrniotavalbN  31066  cdlemb3  31088  cdlemg15  31138  cdlemg17dN  31145  trlco  31209  cdlemg44b  31214  ltrncom  31220  trljco  31222  tendococl  31254  tendoplcl  31263  tendoplcom  31264  tendotr  31312  cdlemk36  31395  cdlemk35s-id  31420  cdlemk39s-id  31422  cdlemk19x  31425  cdlemk53b  31438  cdlemk55  31443  cdlemk35u  31446  cdlemk55u  31448  cdlemk39u  31450  cdlemk19u  31452  cdlemk56  31453  tendoex  31457  cdleml5N  31462  dihord2pre  31708  dihord6apre  31739  dihord5b  31742  dihord5apre  31745  dihord  31747  dihmeetlem1N  31773  dihmeetlem2N  31782  dihglbcpreN  31783  dihmeetbN  31786  dihmeetlem4preN  31789  dihmeetlem5  31791  dihmeetlem6  31792  dihmeetlem7N  31793  dihmeetlem10N  31799  dihmeetlem11N  31800  dihmeetlem12N  31801  dihmeetlem13N  31802  dihmeetlem15N  31804  dihmeetlem17N  31806  dihmeetlem18N  31807  dihmeetlem19N  31808  dihmeetALTN  31810  dih1dimatlem0  31811  dihlspsnssN  31815  dvh3dim2  31931
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