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

Theorem simpl3 963
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 960 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ch )
21adantr 453 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  simpll3  999  simprl3  1005  simp1l3  1053  simp2l3  1059  simp3l3  1065  3anandirs  1287  fcofo  6022  soisores  6048  weniso  6076  knatar  6081  smorndom  6631  nnmord  6876  nnmword  6877  difsnen  7191  mapunen  7277  ac6sfi  7352  fipreima  7413  wemaplem2  7517  en2eqpr  7892  indcardi  7923  acndom  7933  fodomfi2  7942  infmap2  8099  cflim2  8144  coftr  8154  infpssrlem4  8187  fin23lem11  8198  fincssdom  8204  isf32lem9  8242  fin1a2lem9  8289  gchpwdom  8550  gruima  8678  prpssnq  8868  distrlem4pr  8904  addcan  9251  addcan2  9252  ledivmul2OLD  9889  supmul1  9974  uzsupss  10569  xaddass  10829  xleadd1a  10833  xlesubadd  10843  xmulasslem3  10866  xadddilem  10874  xadddi  10875  ixxun  10933  icoshftf1o  11021  modsubdir  11286  ltexp2a  11432  leexp2  11435  ltexp2r  11437  exple1  11440  expnlbnd2  11511  hashtpg  11692  ccatass  11751  ccatopth  11777  s2f1o  11864  limsuplt  12274  limsupgre  12276  addcn2  12388  mulcn2  12390  dvdsmod  12907  gcdass  13046  rplpwr  13057  rppwr  13058  rpmulgcd2  13106  rpexp  13121  rpdvds  13125  prmdiveq  13176  coprimeprodsq  13184  coprimeprodsq2  13185  pythagtriplem3  13193  pcdvdsb  13243  pcgcd1  13251  pcbc  13270  0ram  13389  ramz2  13393  ramub1lem1  13395  mremre  13830  mrieqv2d  13865  lubun  14551  issubmnd  14725  gsumccat  14788  frmdss2  14809  mulgnn0p1  14902  mulgnnsubcl  14903  mulgneg  14909  mulgdirlem  14915  nmzsubg  14982  ghmmulg  15019  odmodnn0  15179  oddvdsnn0  15183  odnncl  15184  odmod  15185  oddvds  15186  odeq  15189  odmulgid  15191  odmulg  15193  odmulgeq  15194  odbezout  15195  odf1o1  15207  odf1o2  15208  odngen  15212  odcau  15239  pgpssslw  15249  fislw  15260  lsmless1x  15279  lsmless2x  15280  lsmsubm  15288  lsmmod  15308  lsmmod2  15309  efgsfo  15372  cntzcmn  15460  odadd1  15464  odadd2  15465  odadd  15466  lsmcomx  15472  prdscmnd  15477  gsumconst  15533  rng1eq0  15703  cntzsubr  15901  isabvd  15909  lspss  16061  0lmhm  16117  reslmhm2  16130  lbspss  16155  lspfixed  16201  lsmcv  16214  lspsnat  16218  issubassa  16384  aspss  16392  coe1subfv  16660  coe1tm  16666  xrsdsreclblem  16745  obselocv  16956  neiint  17169  topssnei  17189  cnrest2  17351  cnprest2  17355  cnt0  17411  cnt1  17415  cnhaus  17419  cncmp  17456  fiuncmp  17468  sscmp  17469  hauscmp  17471  cnconn  17486  uncon  17493  kgen2ss  17588  ptpjopn  17645  ptrescn  17672  qtopss  17748  kqfvima  17763  r0cld  17771  cmphaushmeo  17833  fbssint  17871  fbasrn  17917  filuni  17918  ufilmax  17940  fin1aufil  17965  fmf  17978  fmss  17979  rnelfmlem  17985  rnelfm  17986  fmufil  17992  fmco  17994  flimss2  18005  flimss1  18006  flimrest  18016  cnpflf2  18033  cnpflf  18034  flfcnp  18037  lmflf  18038  supnfcls  18053  fclsss1  18055  fclsss2  18056  cnpfcfi  18073  subgntr  18137  opnsubg  18138  cldsubg  18141  ustuqtop1  18272  ucncn  18316  bldisj  18429  blgt0  18430  bl2in  18431  blss2ps  18434  blss2  18435  xbln0  18445  blssps  18455  blss  18456  lpbl  18534  blcld  18536  blcls  18537  stdbdmopn  18549  metcnp2  18573  txmetcnp  18578  blval2  18606  restmetu  18618  nmoix  18764  nmoi2  18765  nmoeq0  18771  nmotri  18774  metdsge  18880  metds0  18881  metdseq0  18885  icoopnst  18965  iccpnfhmeo  18971  xrhmeo  18972  nmhmcn  19129  cphsqrcl2  19150  cphsqrcl3  19151  fmcfil  19226  bcthlem5  19282  cmetcusp1OLD  19306  cmetcusp1  19307  pjth  19341  ovolunnul  19397  volun  19440  voliunlem2  19446  itg2const  19633  iblconst  19710  itgconst  19711  limcvallem  19759  dvcnp2  19807  dvcn  19808  deg1mul3le  20040  deg1tmle  20041  ig1pdvds  20100  coe11  20172  dgrmulc  20190  dvply1  20202  aaliou2  20258  efcvx  20366  tanord  20441  logdivlti  20516  logccv  20555  recxpcl  20567  cxplea  20588  cxple2a  20591  ang180  20657  isosctrlem2  20664  cxp2lim  20816  amgm  20830  muval1  20917  dvdssqf  20922  mumullem2  20964  bcmono  21062  lgsneg  21104  lgsmod  21106  lgsdirprm  21114  lgsdir  21115  lgsdi  21117  cyclispthon  21621  vdgrfif  21671  zerdivemp1  22023  nvmul0or  22134  shless  22862  shlej1  22863  pjspansn  23080  kbmul  23459  homco2  23481  kbass2  23621  snunioc  24138  eliccelico  24141  elicoelioo  24142  iocinioc2  24143  difioo  24146  xrge0npcan  24217  isarchi2  24256  pstmfval  24292  fmcncfil  24318  zrhnm  24354  qqhnm  24375  volfiniune  24587  probinc  24680  cndprob01  24694  cvmsss2  24962  dedekind  25188  binomrisefac  25359  dvdspw  25370  funsseq  25394  sltres  25620  brbtwn2  25845  colinearalglem1  25846  colinearalg  25850  axcgrtr  25855  axcontlem2  25905  cgrtriv  25937  5segofs  25941  btwntriv2  25947  btwnxfr  25991  segcon2  26040  brsegle2  26044  seglelin  26051  outsideofeu  26066  bpolydif  26102  mblfinlem2  26245  comppfsc  26388  blbnd  26497  rrndstprj2  26541  zerdivemp1x  26572  ofmpteq  26777  mzpsubst  26806  diophrw  26818  eldioph2lem1  26819  rencldnfi  26883  pellexlem2  26894  pellqrexplicit  26941  infmrgelbi  26942  rmxycomplete  26981  congadd  27032  acongeq  27049  jm2.19  27065  jm2.22  27067  jm2.20nn  27069  jm2.25lem1  27070  jm2.27  27080  jm3.1  27092  lmhmlnmsplit  27163  pwssplit0  27165  pwssplit1  27166  pwssplit4  27169  frlmsplit2  27221  frlmsslss2  27223  frlmup4  27231  lindff1  27268  lsslindf  27278  lsslinds  27279  islindf4  27286  hbtlem2  27306  dgraa0p  27332  pmtrfv  27373  pmtrmvd  27376  pmtrfb  27384  idomrootle  27489  hashgcdlem  27494  proot1hash  27497  fmul01  27687  ibliccsinexp  27722  iblioosinexp  27724  stoweidlem20  27746  stoweidlem22  27748  stoweidlem34  27760  stoweidlem44  27770  stoweidlem60  27786  wallispilem3  27793  fzo1fzo0n0  28129  modaddmulmod  28159  modifeq2int  28162  swrdnd  28183  swrdvalodmlem1  28188  swrdccatin12lem3a  28209  swrdccatin12  28215  swrdccat3  28216  4cyclusnfrgra  28410  lubunNEW  29772  lsmsat  29807  lsatfixedN  29808  lssat  29815  lkrlsp  29901  lshpkrlem4  29912  op1cl  29984  cvrcon3b  30076  leat3  30094  atlen0  30109  atnle  30116  atlatmstc  30118  atlatle  30119  cvlcvr1  30138  cvlsupr2  30142  hlsupr2  30185  hlrelat2  30201  cvrexchlem  30217  cvratlem  30219  lnnat  30225  atexchcvrN  30238  1cvratlt  30272  1cvrjat  30273  3atlem3  30283  3atlem7  30287  llni2  30310  atcvrlln2  30317  llnexatN  30319  llncmp  30320  2llnmat  30322  2at0mat0  30323  2atnelpln  30342  llncvrlpln2  30355  2lplnmN  30357  2llnmj  30358  lplncmp  30360  lplnexatN  30361  2llnjaN  30364  lvoli3  30375  islvol2aN  30390  4atlem3a  30395  4atlem4a  30397  4atlem4b  30398  4atlem11  30407  4atlem12  30410  lplncvrlvol2  30413  lvolcmp  30415  2lplnmj  30420  islinei  30538  linepmap  30573  lneq2at  30576  2llnma3r  30586  elpaddn0  30598  elpaddatriN  30601  elpaddat  30602  paddcom  30611  paddss1  30615  paddss2  30616  paddasslem6  30623  paddasslem7  30624  paddasslem10  30627  paddasslem15  30632  pmodlem2  30645  pmodl42N  30649  pmapjoin  30650  atmod1i1m  30656  llnmod1i2  30658  llnexchb2lem  30666  polcon2bN  30718  pclfinclN  30748  poml4N  30751  poml6N  30753  osumcllem11N  30764  osumclN  30765  pmapojoinN  30766  pexmidlem2N  30769  pexmidlem3N  30770  pexmidlem4N  30771  pexmidlem6N  30773  pexmidlem7N  30774  pl42lem2N  30778  pl42lem3N  30779  pl42lem4N  30780  pl42N  30781  lhpexle3lem  30809  lhpmcvr3  30823  lhp2at0nle  30833  lhprelat3N  30838  lauteq  30893  lautco  30895  ltrncoidN  30926  ltrneq2  30946  ltrnnidn  30972  ltrnideq  30973  trlnle  30984  cdlemc  30995  cdlemd4  30999  cdlemd5  31000  cdlemd9  31004  cdlemd  31005  ltrneq3  31006  cdlemefrs29pre00  31193  cdlemefrs29cpre1  31196  cdlemefrs29clN  31197  cdlemefrs32fva  31198  cdlemefr29exN  31200  cdlemefr27cl  31201  cdlemefs27cl  31211  cdlemefs32sn1aw  31212  cdleme32fva  31235  cdleme32d  31242  cdleme32f  31244  cdleme32le  31245  cdleme40n  31266  cdleme41snaw  31274  cdleme17d3  31294  cdleme48fvg  31298  cdlemeg46fvcl  31304  cdlemeg46fgN  31332  cdleme48fgv  31336  ltrniotavalbN  31382  cdlemb3  31404  cdlemg15  31454  cdlemg17dN  31461  trlco  31525  cdlemg44b  31530  ltrncom  31536  trljco  31538  tendococl  31570  tendoplcl  31579  tendoplcom  31580  tendotr  31628  cdlemk36  31711  cdlemk35s-id  31736  cdlemk39s-id  31738  cdlemk19x  31741  cdlemk53b  31754  cdlemk55  31759  cdlemk35u  31762  cdlemk55u  31764  cdlemk39u  31766  cdlemk19u  31768  cdlemk56  31769  tendoex  31773  cdleml5N  31778  dihord2pre  32024  dihord6apre  32055  dihord5b  32058  dihord5apre  32061  dihord  32063  dihmeetlem1N  32089  dihmeetlem2N  32098  dihglbcpreN  32099  dihmeetbN  32102  dihmeetlem4preN  32105  dihmeetlem5  32107  dihmeetlem6  32108  dihmeetlem7N  32109  dihmeetlem10N  32115  dihmeetlem11N  32116  dihmeetlem12N  32117  dihmeetlem13N  32118  dihmeetlem15N  32120  dihmeetlem17N  32122  dihmeetlem18N  32123  dihmeetlem19N  32124  dihmeetALTN  32126  dih1dimatlem0  32127  dihlspsnssN  32131  dvh3dim2  32247
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator