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

Theorem simpl3 960
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 957 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ch )
21adantr 451 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  simpll3  996  simprl3  1002  simp1l3  1050  simp2l3  1056  simp3l3  1062  3anandirs  1284  fcofo  5798  soisores  5824  weniso  5852  knatar  5857  smorndom  6385  nnmord  6630  nnmword  6631  difsnen  6944  mapunen  7030  ac6sfi  7101  fipreima  7161  wemaplem2  7262  en2eqpr  7637  indcardi  7668  acndom  7678  fodomfi2  7687  infmap2  7844  cflim2  7889  coftr  7899  infpssrlem4  7932  fin23lem11  7943  fincssdom  7949  isf32lem9  7987  fin1a2lem9  8034  gchpwdom  8296  gruima  8424  prpssnq  8614  distrlem4pr  8650  addcan  8996  addcan2  8997  ledivmul2OLD  9634  supmul1  9719  uzsupss  10310  xaddass  10569  xleadd1a  10573  xlesubadd  10583  xmulasslem3  10606  xadddilem  10614  xadddi  10615  ixxun  10672  icoshftf1o  10759  modsubdir  11008  ltexp2a  11153  leexp2  11156  ltexp2r  11158  exple1  11161  expnlbnd2  11232  ccatass  11436  ccatopth  11462  limsuplt  11953  limsupgre  11955  addcn2  12067  mulcn2  12069  dvdsmod  12585  gcdass  12724  rplpwr  12735  rppwr  12736  rpmulgcd2  12784  rpexp  12799  rpdvds  12803  prmdiveq  12854  coprimeprodsq  12862  coprimeprodsq2  12863  pythagtriplem3  12871  pcdvdsb  12921  pcgcd1  12929  pcbc  12948  0ram  13067  ramz2  13071  ramub1lem1  13073  mremre  13506  mrieqv2d  13541  lubun  14227  issubmnd  14401  gsumccat  14464  frmdss2  14485  mulgnn0p1  14578  mulgnnsubcl  14579  mulgneg  14585  mulgdirlem  14591  nmzsubg  14658  ghmmulg  14695  odmodnn0  14855  oddvdsnn0  14859  odnncl  14860  odmod  14861  oddvds  14862  odeq  14865  odmulgid  14867  odmulg  14869  odmulgeq  14870  odbezout  14871  odf1o1  14883  odf1o2  14884  odngen  14888  odcau  14915  pgpssslw  14925  fislw  14936  lsmless1x  14955  lsmless2x  14956  lsmsubm  14964  lsmmod  14984  lsmmod2  14985  efgsfo  15048  cntzcmn  15136  odadd1  15140  odadd2  15141  odadd  15142  lsmcomx  15148  prdscmnd  15153  gsumconst  15209  rng1eq0  15379  cntzsubr  15577  isabvd  15585  lspss  15741  0lmhm  15797  reslmhm2  15810  lbspss  15835  lspfixed  15881  lsmcv  15894  lspsnat  15898  issubassa  16064  aspss  16072  coe1subfv  16343  coe1tm  16349  xrsdsreclblem  16417  obselocv  16628  neiint  16841  topssnei  16861  cnrest2  17014  cnprest2  17018  cnt0  17074  cnt1  17078  cnhaus  17082  cncmp  17119  fiuncmp  17131  sscmp  17132  hauscmp  17134  cnconn  17148  uncon  17155  kgen2ss  17250  ptpjopn  17306  ptrescn  17333  qtopss  17406  kqfvima  17421  r0cld  17429  cmphaushmeo  17491  fbssint  17533  fbasrn  17579  filuni  17580  ufilmax  17602  fin1aufil  17627  fmf  17640  fmss  17641  rnelfmlem  17647  rnelfm  17648  fmufil  17654  fmco  17656  flimss2  17667  flimss1  17668  flimrest  17678  cnpflf2  17695  cnpflf  17696  flfcnp  17699  lmflf  17700  supnfcls  17715  fclsss1  17717  fclsss2  17718  cnpfcfi  17735  subgntr  17789  opnsubg  17790  cldsubg  17793  bldisj  17955  blgt0  17956  bl2in  17957  blss2  17959  xbln0  17965  blss  17972  lpbl  18049  blcld  18051  blcls  18052  stdbdmopn  18064  metcnp2  18088  txmetcnp  18093  nmoix  18238  nmoi2  18239  nmoeq0  18245  nmotri  18248  metdsge  18353  metds0  18354  metdseq0  18358  icoopnst  18437  iccpnfhmeo  18443  xrhmeo  18444  nmhmcn  18601  cphsqrcl2  18622  cphsqrcl3  18623  fmcfil  18698  bcthlem5  18750  pjth  18803  ovolunnul  18859  volun  18902  voliunlem2  18908  itg2const  19095  iblconst  19172  itgconst  19173  limcvallem  19221  dvcnp2  19269  dvcn  19270  deg1mul3le  19502  deg1tmle  19503  ig1pdvds  19562  coe11  19634  dgrmulc  19652  dvply1  19664  aaliou2  19720  efcvx  19825  tanord  19900  logdivlti  19971  logccv  20010  recxpcl  20022  cxplea  20043  cxple2a  20046  ang180  20112  isosctrlem2  20119  cxp2lim  20271  amgm  20285  muval1  20371  dvdssqf  20376  mumullem2  20418  bcmono  20516  lgsneg  20558  lgsmod  20560  lgsdirprm  20568  lgsdir  20569  lgsdi  20571  nvmul0or  21210  shless  21938  shlej1  21939  pjspansn  22156  kbmul  22535  homco2  22557  kbass2  22697  cvmsss2  23216  vdgrf  23302  dedekind  23493  dvdspw  23514  funsseq  23536  sltres  23729  brbtwn2  23944  colinearalglem1  23945  colinearalg  23949  axcgrtr  23954  axcontlem2  24004  cgrtriv  24036  5segofs  24040  btwntriv2  24046  btwnxfr  24090  segcon2  24139  brsegle2  24143  seglelin  24150  outsideofeu  24165  bpolydif  24201  sndw  24512  cmprtr  24808  rltrran  24826  rltrooo  24827  zerdivemp1  24848  fgsb2  24967  cmptdst  24980  cmptdst2  24983  limptlimpr2lem1  24986  limptlimpr2lem2  24987  flfnei2  24989  islimrs3  24993  usinuniopb  25006  mslb1  25019  lvsovso  25038  addcanri  25078  isder  25119  clscnc  25422  lppotos  25556  comppfsc  25719  blbnd  25923  rrndstprj2  25967  zerdivemp1x  25998  ofmpteq  26209  mzpsubst  26238  diophrw  26250  eldioph2lem1  26251  rencldnfi  26316  pellexlem2  26327  pellqrexplicit  26374  infmrgelbi  26375  rmxycomplete  26414  congadd  26465  acongeq  26482  jm2.19  26498  jm2.22  26500  jm2.20nn  26502  jm2.25lem1  26503  jm2.27  26513  jm3.1  26525  lmhmlnmsplit  26597  pwssplit0  26599  pwssplit1  26600  pwssplit4  26603  frlmsplit2  26655  frlmsslss2  26657  frlmup4  26665  lindff1  26702  lsslindf  26712  lsslinds  26713  islindf4  26720  hbtlem2  26740  dgraa0p  26766  pmtrfv  26807  pmtrmvd  26810  pmtrfb  26818  idomrootle  26923  hashgcdlem  26928  proot1hash  26931  fmul01  27122  iblioosinexp  27159  stoweidlem20  27181  stoweidlem22  27183  stoweidlem28  27189  stoweidlem34  27195  stoweidlem44  27205  stoweidlem51  27212  stoweidlem60  27221  wallispilem3  27228  s2f1o  27490  lubunNEW  28536  lsmsat  28571  lsatfixedN  28572  lssat  28579  lkrlsp  28665  lshpkrlem4  28676  op1cl  28748  cvrcon3b  28840  leat3  28858  atlen0  28873  atnle  28880  atlatmstc  28882  atlatle  28883  cvlcvr1  28902  cvlsupr2  28906  hlsupr2  28949  hlrelat2  28965  cvrexchlem  28981  cvratlem  28983  lnnat  28989  atexchcvrN  29002  1cvratlt  29036  1cvrjat  29037  3atlem3  29047  3atlem7  29051  llni2  29074  atcvrlln2  29081  llnexatN  29083  llncmp  29084  2llnmat  29086  2at0mat0  29087  2atnelpln  29106  llncvrlpln2  29119  2lplnmN  29121  2llnmj  29122  lplncmp  29124  lplnexatN  29125  2llnjaN  29128  lvoli3  29139  islvol2aN  29154  4atlem3a  29159  4atlem4a  29161  4atlem4b  29162  4atlem11  29171  4atlem12  29174  lplncvrlvol2  29177  lvolcmp  29179  2lplnmj  29184  islinei  29302  linepmap  29337  lneq2at  29340  2llnma3r  29350  elpaddn0  29362  elpaddatriN  29365  elpaddat  29366  paddcom  29375  paddss1  29379  paddss2  29380  paddasslem6  29387  paddasslem7  29388  paddasslem10  29391  paddasslem15  29396  pmodlem2  29409  pmodl42N  29413  pmapjoin  29414  atmod1i1m  29420  llnmod1i2  29422  llnexchb2lem  29430  polcon2bN  29482  pclfinclN  29512  poml4N  29515  poml6N  29517  osumcllem11N  29528  osumclN  29529  pmapojoinN  29530  pexmidlem2N  29533  pexmidlem3N  29534  pexmidlem4N  29535  pexmidlem6N  29537  pexmidlem7N  29538  pl42lem2N  29542  pl42lem3N  29543  pl42lem4N  29544  pl42N  29545  lhpexle3lem  29573  lhpmcvr3  29587  lhp2at0nle  29597  lhprelat3N  29602  lauteq  29657  lautco  29659  ltrncoidN  29690  ltrneq2  29710  ltrnnidn  29736  ltrnideq  29737  trlnle  29748  cdlemc  29759  cdlemd4  29763  cdlemd5  29764  cdlemd9  29768  cdlemd  29769  ltrneq3  29770  cdlemefrs29pre00  29957  cdlemefrs29cpre1  29960  cdlemefrs29clN  29961  cdlemefrs32fva  29962  cdlemefr29exN  29964  cdlemefr27cl  29965  cdlemefs27cl  29975  cdlemefs32sn1aw  29976  cdleme32fva  29999  cdleme32d  30006  cdleme32f  30008  cdleme32le  30009  cdleme40n  30030  cdleme41snaw  30038  cdleme17d3  30058  cdleme48fvg  30062  cdlemeg46fvcl  30068  cdlemeg46fgN  30096  cdleme48fgv  30100  ltrniotavalbN  30146  cdlemb3  30168  cdlemg15  30218  cdlemg17dN  30225  trlco  30289  cdlemg44b  30294  ltrncom  30300  trljco  30302  tendococl  30334  tendoplcl  30343  tendoplcom  30344  tendotr  30392  cdlemk36  30475  cdlemk35s-id  30500  cdlemk39s-id  30502  cdlemk19x  30505  cdlemk53b  30518  cdlemk55  30523  cdlemk35u  30526  cdlemk55u  30528  cdlemk39u  30530  cdlemk19u  30532  cdlemk56  30533  tendoex  30537  cdleml5N  30542  dihord2pre  30788  dihord6apre  30819  dihord5b  30822  dihord5apre  30825  dihord  30827  dihmeetlem1N  30853  dihmeetlem2N  30862  dihglbcpreN  30863  dihmeetbN  30866  dihmeetlem4preN  30869  dihmeetlem5  30871  dihmeetlem6  30872  dihmeetlem7N  30873  dihmeetlem10N  30879  dihmeetlem11N  30880  dihmeetlem12N  30881  dihmeetlem13N  30882  dihmeetlem15N  30884  dihmeetlem17N  30886  dihmeetlem18N  30887  dihmeetlem19N  30888  dihmeetALTN  30890  dih1dimatlem0  30891  dihlspsnssN  30895  dvh3dim2  31011
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator