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

Theorem simpll 732
Description: Simplification of a conjunction. (Contributed by NM, 18-Mar-2007.)
Assertion
Ref Expression
simpll  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ph )

Proof of Theorem simpll
StepHypRef Expression
1 id 21 . 2  |-  ( ph  ->  ph )
21ad2antrr 708 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  simp1ll  1021  simp2ll  1025  simp3ll  1029  pm2.61da3ne  2686  rmob  3251  ifboth  3772  prneimg  3980  ordelord  4605  poinxp  4943  soltmin  5275  sofld  5320  f1oprswap  5719  mpteqb  5821  fvmptt  5822  iinpreima  5862  fcof1  6022  soisoi  6050  grprinvlem  6287  fnfvof  6319  dftpos4  6500  tfrlem9a  6649  oaass  6806  oelimcl  6845  nnawordex  6882  oaabs  6889  oaabs2  6890  omabs  6892  qsel  6985  th3qlem1  7012  mapss  7058  boxcutc  7107  omxpenlem  7211  xpmapenlem  7276  mapdom2  7280  unxpdomlem3  7317  f1finf1o  7337  frfi  7354  nnunifi  7360  indexfi  7416  elfi2  7421  elfiun  7437  marypha1lem  7440  supisolem  7477  ordtypelem7  7495  oismo  7511  wdomtr  7545  brwdom3  7552  cnfcomlem  7658  r1ordg  7706  rankval3b  7754  rankonidlem  7756  harcard  7867  infxpenlem  7897  acni2  7929  numacn  7932  fodomacn  7939  mappwen  7995  dfac9  8018  cdalepw  8078  infxpabs  8094  infunsdom1  8095  infunsdom  8096  ackbij1lem15  8116  cfsmolem  8152  infpssrlem5  8189  infpssr  8190  ssfin4  8192  fin2i2  8200  ssfin2  8202  fin23lem24  8204  fin23lem22  8209  fin23lem27  8210  fin23lem36  8230  isf32lem3  8237  isf32lem7  8241  isf34lem7  8261  fin1a2lem13  8294  hsmexlem4  8311  axdc4lem  8337  iundom2g  8417  alephexp1  8456  fpwwe2lem1  8508  fpwwe2lem8  8514  canthp1  8531  inttsk  8651  inar1  8652  r1tskina  8659  grur1  8697  nqerf  8809  distrlem1pr  8904  distrlem4pr  8905  reclem2pr  8927  addsub4  9346  le2add  9512  lt2sub  9528  le2sub  9529  mulge0  9547  receu  9669  rec11  9714  rec11r  9715  divdivdiv  9717  ddcan  9730  divadddiv  9731  divsubdiv  9732  conjmul  9733  rereccl  9734  subrec  9845  recgt0  9856  prodgt0  9857  prodge0  9859  ltmul12a  9868  lemul12a  9870  lemulge11  9874  lt2mul2div  9888  ltrec  9893  lerec  9894  lt2msq  9896  le2msq  9912  msq11  9913  ledivp1  9914  rimul  9993  zsupss  10567  uzwo3  10571  qreccl  10596  rpnnen1lem1  10602  rpnnen1lem2  10603  rpnnen1lem3  10604  rpnnen1lem5  10606  qbtwnre  10787  qbtwnxr  10788  xralrple  10793  xpncan  10832  xaddge0  10839  xle2add  10840  xmulneg1  10850  xmulgt0  10864  ixxss1  10936  ixxss2  10937  elioc2  10975  difreicc  11030  fzass4  11092  fzrev  11110  modid  11272  uzindi  11322  seqfeq3  11375  seqof2  11383  expcl2lem  11395  expnegz  11416  expadd  11424  expmul  11427  expcan  11434  ltexp2  11435  leexp1a  11440  expnlbnd  11511  digit1  11515  bcval5  11611  bcpasc  11614  hashprb  11670  fzsdom2  11695  hashbclem  11703  hashbc  11704  hashf1lem2  11707  seqcoll  11714  ccatswrd  11775  revccat  11800  sqrmul  12067  sqrlt  12069  sqrdiv  12073  absexpz  12112  abslt  12120  absle  12121  abssubne0  12122  rexico  12159  amgm2  12175  rlim3  12294  lo1bdd2  12320  climuni  12348  rlimcn1  12384  cn1lem  12393  iserex  12452  iserle  12455  isercolllem1  12460  climcau  12466  caucvgb  12475  iseralt  12480  summo  12513  zsum  12514  sumss2  12522  isumadd  12553  fsum2dlem  12556  fsum2d  12557  fsum0diag2  12568  fsumabs  12582  cvgcmp  12597  cvgcmpce  12599  incexclem  12618  incexc2  12620  isumsplit  12622  climcnds  12633  divrcnv  12634  geolim  12649  geo2lim  12654  geomulcvg  12655  mertenslem1  12663  mertenslem2  12664  mertens  12665  efcvgfsum  12690  eftlcl  12710  reeftlcl  12711  tanadd  12770  eirr  12806  rpnnen2  12827  sqr2irr  12850  dvds2ln  12882  dvdseq  12899  dvdsext  12902  bitsfzo  12949  sadadd2lem2  12964  sadadd  12981  bitsshft  12989  smupvallem  12997  smumul  13007  bezout  13044  gcdmultiplez  13053  dvdsmulgcd  13056  prmdvdsexp  13116  pcqmul  13229  pcexp  13235  pcneg  13249  pcdvdstr  13251  pcprmpw2  13257  pcfac  13270  expnprm  13273  prmpwdvds  13274  prmreclem6  13291  mul4sq  13324  vdwapf  13342  vdwlem13  13363  vdw  13364  vdwnnlem3  13367  vdwnn  13368  ramub2  13384  ramz  13395  ramcl  13399  ressress  13528  pwsle  13716  mreriincl  13825  mrcuni  13848  mreexexlemd  13871  isacs2  13880  acsfn  13886  acsfn1  13888  acsfn2  13890  iscat  13899  cidfval  13903  iscatd2  13908  monfval  13960  isfunc  14063  isfull2  14110  isfth2  14114  1stfval  14290  2ndfval  14293  yonedainv  14380  drsdirfi  14397  pospo  14432  mod1ile  14536  mod2ile  14537  isipodrs  14589  isacs4lem  14596  mrelatlub  14614  spwpr4  14665  submnd0  14727  resmhm  14761  mhmco  14764  mhmima  14765  pwsdiagmhm  14770  gsumwsubmcl  14786  gsumwmhm  14792  gsumwspan  14793  grprcan  14840  grplactcnv  14889  mulgz  14913  mulgnn0dir  14915  mulgdir  14917  mulgneg2  14919  mulgnn0ass  14921  mhmmulg  14924  pwssub  14933  pwsmulg  14934  issubg4  14963  nmzsubg  14983  ssnmz  14984  ghmmhmb  15019  resghm  15024  ghmpreima  15029  ghmnsgpreima  15032  ghmf1o  15037  isga  15070  gaid  15078  gass  15080  gapm  15085  gaorber  15087  gastacl  15088  gastacos  15089  lactghmga  15109  cntzsubm  15136  cntzsubg  15137  cntzmhm  15139  submod  15205  gexdvds  15220  gexcl3  15223  sylow2blem3  15258  lsmub1x  15282  lsmless12  15297  pj1id  15333  efglem  15350  efgcpbllemb  15389  mulgnn0di  15450  eqgabl  15456  gexex  15470  torsubg  15471  cygabl  15502  prmcyg  15505  cyggexb  15510  gsumval3  15516  subgdmdprd  15594  mgpress  15661  isrng  15670  rngpropd  15697  dvdsrtr  15759  isdrng2  15847  issubrg  15870  cntzsubr  15902  abvrec  15926  abvdiv  15927  islmodd  15958  lmodprop2d  16008  lssvsubcl  16022  lssvacl  16032  lssvscl  16033  islss3  16037  lss1d  16041  lsspropd  16095  islmhm  16105  lmhmco  16121  lmhmplusg  16122  lmhmf1o  16124  lmhmima  16125  lmhmpreima  16126  reslmhm  16130  lspextmo  16134  pwsdiaglmhm  16135  lmhmpropd  16147  islbs2  16228  lidlsubcl  16289  drngnidl  16302  2idlcpbl  16307  unitrrg  16355  fidomndrng  16369  issubassa  16385  assapropd  16388  psrbaglefi  16439  psrbagconf1o  16441  coe1mul2lem1  16662  ply1coe  16686  qsssubdrg  16760  cnsubrg  16761  zlpir  16773  domnchr  16815  znval  16818  znunit  16846  znrrg  16848  isphl  16861  ocvlss  16901  ocvin  16903  obslbs  16959  toponmre  17159  neissex  17193  clslp  17214  tgrest  17225  restcld  17238  ssrest  17242  restopn2  17243  pnfnei  17286  mnfnei  17287  cnpnei  17330  cnco  17332  cnss1  17342  cnss2  17343  isnrm2  17424  restcnrm  17428  dnsconst  17444  cmpsub  17465  uncmp  17468  dfcon2  17484  2ndcrest  17519  1stcelcls  17526  hausllycmp  17559  cldllycmp  17560  dislly  17562  kgencn  17590  ptpjpre2  17614  ptclsg  17649  dfac14  17652  txindis  17668  txlly  17670  txnlly  17671  txcmp  17677  xkoptsub  17688  xkopt  17689  xkoinjcn  17721  qtopkgen  17744  kqdisj  17766  kqcldsat  17767  isr0  17771  kqreglem2  17776  kqnrmlem2  17778  nrmr0reg  17783  reghmph  17827  nrmhmph  17828  infil  17897  fgabs  17913  filcon  17917  trfil2  17921  isufil2  17942  trufil  17944  filssufilg  17945  ssufl  17952  ufileu  17953  rnelfm  17987  fbflim  18010  flimclsi  18012  flimsncls  18020  hauspwpwf1  18021  fclsval  18042  fclscf  18059  flimfnfcls  18062  uffclsflim  18065  alexsubb  18079  cnextcn  18100  tmdmulg  18124  symgtgp  18133  utoptop  18266  utopsnneiplem  18279  psmetres2  18347  xmetres2  18393  xblss2ps  18433  blhalf  18437  blssexps  18458  blssex  18459  blin2  18461  blbas  18462  met1stc  18553  met2ndci  18554  metcnpi  18576  metcnpi2  18577  metusttoOLD  18589  metustto  18590  metustexhalfOLD  18595  metustexhalf  18596  elbl4  18608  metuel2  18611  dscopn  18623  ngpinvds  18661  subgngp  18678  tngngp  18697  nmdvr  18708  nlmvscn  18725  nrginvrcn  18729  lssnlm  18738  nmoco  18773  blcvx  18831  tgqioo  18833  icccmplem2  18856  metdstri  18883  metdsle  18884  metdsre  18885  cncfss  18931  icoopnst  18966  phtpycc  19018  phtpc01  19023  pcohtpylem  19046  clmmulg  19120  iscph  19135  ipcn  19202  csscld  19205  clsocv  19206  cfilfcls  19229  cmetcau  19244  iscmet3lem2  19247  lmclim  19257  flimcfil  19268  cmetss  19269  bcth  19284  bcth2  19285  cmetcuspOLD  19309  cmetcusp  19310  ivthicc  19357  ovolficc  19367  ovolctb  19388  ovolun  19397  ovolfiniun  19399  ovoliunlem2  19401  ovoliunlem3  19402  ovolicc2lem3  19417  ovolicc2lem4  19418  unmbl  19434  shftmbl  19435  volfiniun  19443  voliunlem3  19448  volsup  19452  ioombl  19461  volcn  19500  volivth  19501  vitalilem1  19502  mbfconstlem  19523  mbfposr  19546  cnmbf  19553  mbflimsup  19560  i1fd  19575  i1f1  19584  itg10a  19604  itg2le  19633  itg2const2  19635  iblss  19698  itgeqa  19707  bddmulibl  19732  cnplimc  19776  limccnp2  19781  dvres  19800  dvnres  19819  dvcj  19838  dvrec  19843  dvmptfsum  19861  dvexp3  19864  dveflem  19865  dvfsumrlimge0  19916  evlsval  19942  tdeglem4  19985  ply1domn  20048  elply2  20117  ply1termlem  20124  plypf1  20133  plymullem1  20135  dgrlem  20150  coeid  20159  coeeq2  20163  coemulc  20175  dgreq0  20185  dvply2g  20204  plydivalg  20218  plyexmo  20232  elqaa  20241  aaliou3lem8  20264  dvtaylp  20288  mtest  20322  abelthlem2  20350  ptolemy  20406  cosord  20436  logdivle  20519  divlogrlim  20528  logcnlem5  20539  logtayl  20553  cxpmul2  20582  abscxp2  20586  cxplt  20587  cxple  20588  cxplt3  20593  atantayl3  20781  birthdaylem3  20794  rlimcnp2  20807  efrlim  20810  cxploglim2  20819  scvxcvx  20826  fta  20864  efnnfsumcl  20887  isppw2  20900  sqf11  20924  sgmval  20927  sgmval2  20928  efchtdvds  20944  sqff1o  20967  sgmmul  20987  pclogsum  21001  vmasum  21002  logfac2  21003  logexprlim  21011  perfect  21017  dchrelbas4  21029  dchrptlem2  21051  bcmax  21064  bposlem1  21070  bpos  21079  lgslem4  21085  lgsdir2lem5  21113  2sqlem6  21155  dchrisumlem3  21187  dchrmusum2  21190  pntrlog2bnd  21280  pntlem3  21305  pnt3  21308  qabvexp  21322  ostth  21335  umgra1  21363  uslgra1  21394  usgra1  21395  usgraedg4  21408  wlkres  21531  wlkbprop  21536  0pthon  21581  constr2trl  21601  crcts  21611  cycls  21612  constr3trllem5  21643  constr3cycllem1  21647  constr3cyclp  21651  3v3e3cycl  21654  4cycl4v4e  21655  4cycl4dv4e  21657  eupatrl  21692  grpoidinvlem4  21797  grpoideu  21799  grpoidinv2  21808  rngo2  21978  blocnilem  22307  ipblnfi  22359  minvecolem4  22384  hvmul0or  22529  his35  22592  pjhtheu2  22920  3oalem2  23167  bralnfn  23453  kbpj  23461  eighmorth  23469  hmopm  23526  hmopco  23528  lnconi  23538  riesz3i  23567  cnlnadjlem6  23577  adjmul  23597  leopmuli  23638  nmopleid  23644  dmdbr2  23808  mdslmd1lem1  23830  superpos  23859  chirredlem2  23896  chirredi  23899  atcvat4i  23902  ifeqeqx  24003  iuninc  24013  abfmpeld  24068  xaddeq0  24121  xreceu  24170  toslub  24193  tosglb  24194  xrsmulgzz  24202  gsumpropd2lem  24222  ofldsqr  24242  ofldchr  24246  pstmxmet  24294  xpinpreima2  24307  sqsscirc2  24309  xrge0iifiso  24323  elzrhunit  24365  qqhf  24372  qqhucn  24378  indpreima  24424  indf1ofs  24425  gsumesum  24453  esumlub  24454  esumpr2  24460  esumfzf  24461  esumfsup  24462  esumpcvgval  24470  esumcvg  24478  sigainb  24521  insiga  24522  measiuns  24573  meascnbl  24575  measinb  24577  measdivcstOLD  24580  measdivcst  24581  dya2iocnrect  24633  dya2iocnei  24634  dya2iocucvr  24636  sibfof  24656  ballotlemfc0  24752  ballotlemfcc  24753  ballotlemsima  24775  gamcvg2lem  24845  subfacp1lem6  24873  pconcon  24920  conpcon  24924  sconpi1  24928  txscon  24930  cnllyscon  24934  cvmopnlem  24967  cvmfolem  24968  cvmlift  24988  sinccvg  25112  relexp0  25131  relexpindlem  25141  divelunit  25187  mulge0b  25193  ntrivcvgmullem  25231  prodmolem2  25263  prodmo  25264  zprod  25265  fprod2dlem  25306  risefallfac  25342  fallfacfwd  25354  sltval2  25613  nodense  25646  nofulllem4  25662  colinearalglem4  25850  axcontlem2  25906  axcontlem4  25908  axcontlem7  25911  axcontlem8  25912  axcontlem9  25913  axcontlem10  25914  btwncomim  25949  btwnswapid  25953  lineext  26012  btwnconn1lem11  26033  btwnconn1lem14  26036  broutsideof3  26062  outsideoftr  26065  outsidele  26068  ellines  26088  linethru  26089  lxflflp1  26243  mblfinlem1  26245  mblfinlem2  26246  mblfinlem3  26247  ismblfin  26249  itg2addnclem  26258  itg2addnclem2  26259  itg2addnc  26261  ftc1anclem5  26286  ftc1anclem7  26288  locfindis  26387  neibastop2lem  26391  neibastop2  26392  sdclem1  26449  geomcau  26467  isbnd3  26495  prdsbnd2  26506  ismtyhmeo  26516  heibor1  26521  rrnmet  26540  rrndstprj1  26541  rrncmslem  26543  rrncms  26544  iccbnd  26551  prter3  26733  elrfirn2  26752  mrefg3  26764  isnacs3  26766  mzprename  26808  rexrabdioph  26856  icodiamlt  26885  pellexlem3  26896  pellex  26900  pellqrex  26944  pellfundex  26951  pellfund14b  26964  monotoddzzfi  27007  rpexpmord  27013  jm2.24  27030  congsym  27035  acongtr  27045  bezoutr  27052  bezoutr1  27053  jm2.18  27061  harinf  27107  kelac1  27140  lnmlsslnm  27158  dsmmbas2  27182  dsmmfi  27183  frlmlbs  27228  isnumbasgrplem3  27249  lindfind  27265  lindfrn  27270  islindf3  27275  hbt  27313  dgraalem  27329  mpaaeu  27334  f1omvdconj  27368  pmtrfinv  27381  symggen  27390  psgnunilem3  27398  grpvrinv  27430  matrng  27459  matassa  27460  mat1  27461  mendlmod  27480  acsfn1p  27486  proot1mul  27494  ofmul12  27521  ofdivdiv2  27524  refsumcn  27679  fmul01lt1lem1  27692  climsuselem1  27711  climsuse  27712  stoweidlem7  27734  stoweidlem14  27741  stoweidlem19  27746  stoweidlem20  27747  stoweidlem26  27753  stoweidlem31  27758  stoweidlem34  27761  stoweidlem39  27766  stoweidlem44  27771  stoweidlem46  27773  stoweidlem48  27775  stoweidlem59  27786  stoweidlem60  27787  stirlinglem5  27805  afvco2  28018  ndmaovdistr  28049  2f1fvneq  28083  imarnf1pr  28090  elovmpt3rab1  28095  uzletr  28114  elfz2z  28116  2elfz2melfz  28128  fzonmapblen  28145  hashimarn  28174  swrdvalodm2  28210  swdeq  28218  swrdccatin12lem3  28234  swrdccatin12lem4  28235  swrdccatin12  28236  swrdccat3  28237  2cshw  28278  lswrdn0  28282  cshweqdif2s  28293  cshwssizelem3  28304  usgra2pthspth  28331  wwlkiswwlkn  28372  el2wlkonotot1  28394  usg2spthonot0  28409  usg2spthonot1  28410  usgravd00  28424  2pthfrgra  28463  frgrancvvdeqlemC  28490  frgrawopreglem4  28498  onfrALTlem2  28694  2pm13.193  28701  onfrALTlem2VD  29063  lssats  29872  lfl0f  29929  ncvr1  30132  cvrletrN  30133  cvrnrefN  30142  iscvlat2N  30184  ltltncvr  30282  atcvrj2b  30291  atltcvr  30294  cvrat4  30302  islln3  30369  llnle  30377  2at0mat0  30384  islpln3  30392  islpln5  30394  islpln2a  30407  islvol3  30435  pmapglb2N  30630  pmapglb2xN  30631  isline3  30635  isline4N  30636  pmod1i  30707  pclbtwnN  30756  pclfinN  30759  pexmidN  30828  pexmidlem8N  30836  lhplt  30859  lhpexle1  30867  lhpjat1  30879  lhpj1  30881  lhpmcvr  30882  lhpmcvr2  30883  lhpm0atN  30888  lautcvr  30951  ldil1o  30971  ldilcnv  30974  ltrn1o  30983  idltrn  31009  cdlemc3  31052  cdlemc4  31053  cdlemd1  31057  cdleme0cp  31073  cdleme0cq  31074  cdlemeulpq  31079  cdleme1  31086  cdleme2  31087  cdleme3b  31088  cdleme3c  31089  cdlemedb  31156  cdleme27a  31226  cdlemefrs32fva  31259  cdleme42keg  31345  cdleme42mgN  31347  cdleme48gfv  31396  cdlemf2  31421  cdlemg1cex  31447  cdlemg5  31464  cdlemg4c  31471  trlcoat  31582  tgrpgrplem  31608  tendodi1  31643  tendodi2  31644  tendo0pl  31650  tendoicl  31655  tendoipl  31656  tendo0mul  31685  tendo0mulr  31686  dva1dim  31844  erngdvlem4  31850  erngdvlem4-rN  31858  tendospdi1  31880  dialss  31906  diaglbN  31915  diameetN  31916  dibglbN  32026  dib1dim2  32028  diblss  32030  dicssdvh  32046  diclss  32053  diclspsn  32054  dihlsscpre  32094  dihglblem5aN  32152  dihglblem4  32157  dihglblem5  32158  dih1dimatlem  32189  dihlsprn  32191  dihatlat  32194  dihglblem6  32200  dochvalr  32217
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
  Copyright terms: Public domain W3C validator