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

Theorem simpll 731
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 20 . 2  |-  ( ph  ->  ph )
21ad2antrr 707 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  simp1ll  1020  simp2ll  1024  simp3ll  1028  pm2.61da3ne  2647  rmob  3209  ifboth  3730  prneimg  3938  ordelord  4563  poinxp  4900  soltmin  5232  sofld  5277  f1oprswap  5676  mpteqb  5778  fvmptt  5779  iinpreima  5819  fcof1  5979  soisoi  6007  grprinvlem  6244  fnfvof  6276  dftpos4  6457  tfrlem9a  6606  oaass  6763  oelimcl  6802  nnawordex  6839  oaabs  6846  oaabs2  6847  omabs  6849  qsel  6942  th3qlem1  6969  mapss  7015  boxcutc  7064  omxpenlem  7168  xpmapenlem  7233  mapdom2  7237  unxpdomlem3  7274  f1finf1o  7294  frfi  7311  nnunifi  7317  indexfi  7372  elfi2  7377  elfiun  7393  marypha1lem  7396  supisolem  7431  ordtypelem7  7449  oismo  7465  wdomtr  7499  brwdom3  7506  cnfcomlem  7612  r1ordg  7660  rankval3b  7708  rankonidlem  7710  harcard  7821  infxpenlem  7851  acni2  7883  numacn  7886  fodomacn  7893  mappwen  7949  dfac9  7972  cdalepw  8032  infxpabs  8048  infunsdom1  8049  infunsdom  8050  ackbij1lem15  8070  cfsmolem  8106  infpssrlem5  8143  infpssr  8144  ssfin4  8146  fin2i2  8154  ssfin2  8156  fin23lem24  8158  fin23lem22  8163  fin23lem27  8164  fin23lem36  8184  isf32lem3  8191  isf32lem7  8195  isf34lem7  8215  fin1a2lem13  8248  hsmexlem4  8265  axdc4lem  8291  iundom2g  8371  alephexp1  8410  fpwwe2lem1  8462  fpwwe2lem8  8468  canthp1  8485  inttsk  8605  inar1  8606  r1tskina  8613  grur1  8651  nqerf  8763  distrlem1pr  8858  distrlem4pr  8859  reclem2pr  8881  addsub4  9300  le2add  9466  lt2sub  9482  le2sub  9483  mulge0  9501  receu  9623  rec11  9668  rec11r  9669  divdivdiv  9671  ddcan  9684  divadddiv  9685  divsubdiv  9686  conjmul  9687  rereccl  9688  subrec  9799  recgt0  9810  prodgt0  9811  prodge0  9813  ltmul12a  9822  lemul12a  9824  lemulge11  9828  lt2mul2div  9842  ltrec  9847  lerec  9848  lt2msq  9850  le2msq  9866  msq11  9867  ledivp1  9868  rimul  9947  zsupss  10521  uzwo3  10525  qreccl  10550  rpnnen1lem1  10556  rpnnen1lem2  10557  rpnnen1lem3  10558  rpnnen1lem5  10560  qbtwnre  10741  qbtwnxr  10742  xralrple  10747  xpncan  10786  xaddge0  10793  xle2add  10794  xmulneg1  10804  xmulgt0  10818  ixxss1  10890  ixxss2  10891  elioc2  10929  difreicc  10984  fzass4  11046  fzrev  11064  modid  11225  uzindi  11275  seqfeq3  11328  seqof2  11336  expcl2lem  11348  expnegz  11369  expadd  11377  expmul  11380  expcan  11387  ltexp2  11388  leexp1a  11393  expnlbnd  11464  digit1  11468  bcval5  11564  bcpasc  11567  hashprb  11623  fzsdom2  11648  hashbclem  11656  hashbc  11657  hashf1lem2  11660  seqcoll  11667  ccatswrd  11728  revccat  11753  sqrmul  12020  sqrlt  12022  sqrdiv  12026  absexpz  12065  abslt  12073  absle  12074  abssubne0  12075  rexico  12112  amgm2  12128  rlim3  12247  lo1bdd2  12273  climuni  12301  rlimcn1  12337  cn1lem  12346  iserex  12405  iserle  12408  isercolllem1  12413  climcau  12419  caucvgb  12428  iseralt  12433  summo  12466  zsum  12467  sumss2  12475  isumadd  12506  fsum2dlem  12509  fsum2d  12510  fsum0diag2  12521  fsumabs  12535  cvgcmp  12550  cvgcmpce  12552  incexclem  12571  incexc2  12573  isumsplit  12575  climcnds  12586  divrcnv  12587  geolim  12602  geo2lim  12607  geomulcvg  12608  mertenslem1  12616  mertenslem2  12617  mertens  12618  efcvgfsum  12643  eftlcl  12663  reeftlcl  12664  tanadd  12723  eirr  12759  rpnnen2  12780  sqr2irr  12803  dvds2ln  12835  dvdseq  12852  dvdsext  12855  bitsfzo  12902  sadadd2lem2  12917  sadadd  12934  bitsshft  12942  smupvallem  12950  smumul  12960  bezout  12997  gcdmultiplez  13006  dvdsmulgcd  13009  prmdvdsexp  13069  pcqmul  13182  pcexp  13188  pcneg  13202  pcdvdstr  13204  pcprmpw2  13210  pcfac  13223  expnprm  13226  prmpwdvds  13227  prmreclem6  13244  mul4sq  13277  vdwapf  13295  vdwlem13  13316  vdw  13317  vdwnnlem3  13320  vdwnn  13321  ramub2  13337  ramz  13348  ramcl  13352  ressress  13481  pwsle  13669  mreriincl  13778  mrcuni  13801  mreexexlemd  13824  isacs2  13833  acsfn  13839  acsfn1  13841  acsfn2  13843  iscat  13852  cidfval  13856  iscatd2  13861  monfval  13913  isfunc  14016  isfull2  14063  isfth2  14067  1stfval  14243  2ndfval  14246  yonedainv  14333  drsdirfi  14350  pospo  14385  mod1ile  14489  mod2ile  14490  isipodrs  14542  isacs4lem  14549  mrelatlub  14567  spwpr4  14618  submnd0  14680  resmhm  14714  mhmco  14717  mhmima  14718  pwsdiagmhm  14723  gsumwsubmcl  14739  gsumwmhm  14745  gsumwspan  14746  grprcan  14793  grplactcnv  14842  mulgz  14866  mulgnn0dir  14868  mulgdir  14870  mulgneg2  14872  mulgnn0ass  14874  mhmmulg  14877  pwssub  14886  pwsmulg  14887  issubg4  14916  nmzsubg  14936  ssnmz  14937  ghmmhmb  14972  resghm  14977  ghmpreima  14982  ghmnsgpreima  14985  ghmf1o  14990  isga  15023  gaid  15031  gass  15033  gapm  15038  gaorber  15040  gastacl  15041  gastacos  15042  lactghmga  15062  cntzsubm  15089  cntzsubg  15090  cntzmhm  15092  submod  15158  gexdvds  15173  gexcl3  15176  sylow2blem3  15211  lsmub1x  15235  lsmless12  15250  pj1id  15286  efglem  15303  efgcpbllemb  15342  mulgnn0di  15403  eqgabl  15409  gexex  15423  torsubg  15424  cygabl  15455  prmcyg  15458  cyggexb  15463  gsumval3  15469  subgdmdprd  15547  mgpress  15614  isrng  15623  rngpropd  15650  dvdsrtr  15712  isdrng2  15800  issubrg  15823  cntzsubr  15855  abvrec  15879  abvdiv  15880  islmodd  15911  lmodprop2d  15961  lssvsubcl  15975  lssvacl  15985  lssvscl  15986  islss3  15990  lss1d  15994  lsspropd  16048  islmhm  16058  lmhmco  16074  lmhmplusg  16075  lmhmf1o  16077  lmhmima  16078  lmhmpreima  16079  reslmhm  16083  lspextmo  16087  pwsdiaglmhm  16088  lmhmpropd  16100  islbs2  16181  lidlsubcl  16242  drngnidl  16255  2idlcpbl  16260  unitrrg  16308  fidomndrng  16322  issubassa  16338  assapropd  16341  psrbaglefi  16392  psrbagconf1o  16394  coe1mul2lem1  16615  ply1coe  16639  qsssubdrg  16713  cnsubrg  16714  zlpir  16726  domnchr  16768  znval  16771  znunit  16799  znrrg  16801  isphl  16814  ocvlss  16854  ocvin  16856  obslbs  16912  toponmre  17112  neissex  17146  clslp  17166  tgrest  17177  restcld  17190  ssrest  17194  restopn2  17195  pnfnei  17238  mnfnei  17239  cnpnei  17282  cnco  17284  cnss1  17294  cnss2  17295  isnrm2  17376  restcnrm  17380  dnsconst  17396  cmpsub  17417  uncmp  17420  dfcon2  17435  2ndcrest  17470  1stcelcls  17477  hausllycmp  17510  cldllycmp  17511  dislly  17513  kgencn  17541  ptpjpre2  17565  ptclsg  17600  dfac14  17603  txindis  17619  txlly  17621  txnlly  17622  txcmp  17628  xkoptsub  17639  xkopt  17640  xkoinjcn  17672  qtopkgen  17695  kqdisj  17717  kqcldsat  17718  isr0  17722  kqreglem2  17727  kqnrmlem2  17729  nrmr0reg  17734  reghmph  17778  nrmhmph  17779  infil  17848  fgabs  17864  filcon  17868  trfil2  17872  isufil2  17893  trufil  17895  filssufilg  17896  ssufl  17903  ufileu  17904  rnelfm  17938  fbflim  17961  flimclsi  17963  flimsncls  17971  hauspwpwf1  17972  fclsval  17993  fclscf  18010  flimfnfcls  18013  uffclsflim  18016  alexsubb  18030  cnextcn  18051  tmdmulg  18075  symgtgp  18084  utoptop  18217  utopsnneiplem  18230  psmetres2  18298  xmetres2  18344  xblss2ps  18384  blhalf  18388  blssexps  18409  blssex  18410  blin2  18412  blbas  18413  met1stc  18504  met2ndci  18505  metcnpi  18527  metcnpi2  18528  metusttoOLD  18540  metustto  18541  metustexhalfOLD  18546  metustexhalf  18547  elbl4  18559  metuel2  18562  dscopn  18574  ngpinvds  18612  subgngp  18629  tngngp  18648  nmdvr  18659  nlmvscn  18676  nrginvrcn  18680  lssnlm  18689  nmoco  18724  blcvx  18782  tgqioo  18784  icccmplem2  18807  metdstri  18834  metdsle  18835  metdsre  18836  cncfss  18882  icoopnst  18917  phtpycc  18969  phtpc01  18974  pcohtpylem  18997  clmmulg  19071  iscph  19086  ipcn  19153  csscld  19156  clsocv  19157  cfilfcls  19180  cmetcau  19195  iscmet3lem2  19198  lmclim  19208  flimcfil  19219  cmetss  19220  bcth  19235  bcth2  19236  cmetcuspOLD  19260  cmetcusp  19261  ivthicc  19308  ovolficc  19318  ovolctb  19339  ovolun  19348  ovolfiniun  19350  ovoliunlem2  19352  ovoliunlem3  19353  ovolicc2lem3  19368  ovolicc2lem4  19369  unmbl  19385  shftmbl  19386  volfiniun  19394  voliunlem3  19399  volsup  19403  ioombl  19412  volcn  19451  volivth  19452  vitalilem1  19453  mbfconstlem  19474  mbfposr  19497  cnmbf  19504  mbflimsup  19511  i1fd  19526  i1f1  19535  itg10a  19555  itg2le  19584  itg2const2  19586  iblss  19649  itgeqa  19658  bddmulibl  19683  cnplimc  19727  limccnp2  19732  dvres  19751  dvnres  19770  dvcj  19789  dvrec  19794  dvmptfsum  19812  dvexp3  19815  dveflem  19816  dvfsumrlimge0  19867  evlsval  19893  tdeglem4  19936  ply1domn  19999  elply2  20068  ply1termlem  20075  plypf1  20084  plymullem1  20086  dgrlem  20101  coeid  20110  coeeq2  20114  coemulc  20126  dgreq0  20136  dvply2g  20155  plydivalg  20169  plyexmo  20183  elqaa  20192  aaliou3lem8  20215  dvtaylp  20239  mtest  20273  abelthlem2  20301  ptolemy  20357  cosord  20387  logdivle  20470  divlogrlim  20479  logcnlem5  20490  logtayl  20504  cxpmul2  20533  abscxp2  20537  cxplt  20538  cxple  20539  cxplt3  20544  atantayl3  20732  birthdaylem3  20745  rlimcnp2  20758  efrlim  20761  cxploglim2  20770  scvxcvx  20777  fta  20815  efnnfsumcl  20838  isppw2  20851  sqf11  20875  sgmval  20878  sgmval2  20879  efchtdvds  20895  sqff1o  20918  sgmmul  20938  pclogsum  20952  vmasum  20953  logfac2  20954  logexprlim  20962  perfect  20968  dchrelbas4  20980  dchrptlem2  21002  bcmax  21015  bposlem1  21021  bpos  21030  lgslem4  21036  lgsdir2lem5  21064  2sqlem6  21106  dchrisumlem3  21138  dchrmusum2  21141  pntrlog2bnd  21231  pntlem3  21256  pnt3  21259  qabvexp  21273  ostth  21286  umgra1  21314  uslgra1  21345  usgra1  21346  usgraedg4  21359  wlkres  21482  wlkbprop  21487  0pthon  21532  constr2trl  21552  crcts  21562  cycls  21563  constr3trllem5  21594  constr3cycllem1  21598  constr3cyclp  21602  3v3e3cycl  21605  4cycl4v4e  21606  4cycl4dv4e  21608  eupatrl  21643  grpoidinvlem4  21748  grpoideu  21750  grpoidinv2  21759  rngo2  21929  blocnilem  22258  ipblnfi  22310  minvecolem4  22335  hvmul0or  22480  his35  22543  pjhtheu2  22871  3oalem2  23118  bralnfn  23404  kbpj  23412  eighmorth  23420  hmopm  23477  hmopco  23479  lnconi  23489  riesz3i  23518  cnlnadjlem6  23528  adjmul  23548  leopmuli  23589  nmopleid  23595  dmdbr2  23759  mdslmd1lem1  23781  superpos  23810  chirredlem2  23847  chirredi  23850  atcvat4i  23853  ifeqeqx  23954  iuninc  23964  abfmpeld  24019  xaddeq0  24072  xreceu  24121  toslub  24144  tosglb  24145  xrsmulgzz  24153  gsumpropd2lem  24173  ofldsqr  24193  ofldchr  24197  pstmxmet  24245  xpinpreima2  24258  sqsscirc2  24260  xrge0iifiso  24274  elzrhunit  24316  qqhf  24323  qqhucn  24329  indpreima  24375  indf1ofs  24376  gsumesum  24404  esumlub  24405  esumpr2  24411  esumfzf  24412  esumfsup  24413  esumpcvgval  24421  esumcvg  24429  sigainb  24472  insiga  24473  measiuns  24524  meascnbl  24526  measinb  24528  measdivcstOLD  24531  measdivcst  24532  dya2iocnrect  24584  dya2iocnei  24585  dya2iocucvr  24587  sibfof  24607  ballotlemfc0  24703  ballotlemfcc  24704  ballotlemsima  24726  gamcvg2lem  24796  subfacp1lem6  24824  pconcon  24871  conpcon  24875  sconpi1  24879  txscon  24881  cnllyscon  24885  cvmopnlem  24918  cvmfolem  24919  cvmlift  24939  sinccvg  25063  relexp0  25082  relexpindlem  25092  divelunit  25138  mulge0b  25144  ntrivcvgmullem  25182  prodmolem2  25214  prodmo  25215  zprod  25216  fprod2dlem  25257  risefallfac  25292  fallfacfwd  25303  sltval2  25524  nodense  25557  nofulllem4  25573  colinearalglem4  25752  axcontlem2  25808  axcontlem4  25810  axcontlem7  25813  axcontlem8  25814  axcontlem9  25815  axcontlem10  25816  btwncomim  25851  btwnswapid  25855  lineext  25914  btwnconn1lem11  25935  btwnconn1lem14  25938  broutsideof3  25964  outsideoftr  25967  outsidele  25970  ellines  25990  linethru  25991  lxflflp1  26142  mblfinlem  26143  mblfinlem2  26144  ismblfin  26146  itg2addnclem  26155  itg2addnclem2  26156  itg2addnc  26158  locfindis  26275  neibastop2lem  26279  neibastop2  26280  sdclem1  26337  geomcau  26355  isbnd3  26383  prdsbnd2  26394  ismtyhmeo  26404  heibor1  26409  rrnmet  26428  rrndstprj1  26429  rrncmslem  26431  rrncms  26432  iccbnd  26439  prter3  26621  elrfirn2  26640  mrefg3  26652  isnacs3  26654  mzprename  26696  rexrabdioph  26744  icodiamlt  26773  pellexlem3  26784  pellex  26788  pellqrex  26832  pellfundex  26839  pellfund14b  26852  monotoddzzfi  26895  rpexpmord  26901  jm2.24  26918  congsym  26923  acongtr  26933  bezoutr  26940  bezoutr1  26941  jm2.18  26949  harinf  26995  kelac1  27029  lnmlsslnm  27047  dsmmbas2  27071  dsmmfi  27072  frlmlbs  27117  isnumbasgrplem3  27138  lindfind  27154  lindfrn  27159  islindf3  27164  hbt  27202  dgraalem  27218  mpaaeu  27223  f1omvdconj  27257  pmtrfinv  27270  symggen  27279  psgnunilem3  27287  grpvrinv  27319  matrng  27348  matassa  27349  mat1  27350  mendlmod  27369  acsfn1p  27375  proot1mul  27383  ofmul12  27410  ofdivdiv2  27413  refsumcn  27568  fmul01lt1lem1  27581  climsuselem1  27600  climsuse  27601  stoweidlem7  27623  stoweidlem14  27630  stoweidlem19  27635  stoweidlem20  27636  stoweidlem26  27642  stoweidlem31  27647  stoweidlem34  27650  stoweidlem39  27655  stoweidlem44  27660  stoweidlem46  27662  stoweidlem48  27664  stoweidlem59  27675  stoweidlem60  27676  stirlinglem5  27694  afvco2  27907  ndmaovdistr  27938  2f1fvneq  27958  imarnf1pr  27965  hashimarn  27994  swrdccatin12lem3a  28021  swrdccatin12lem3  28024  swrdccatin12b  28027  usgra2pthspth  28035  el2wlkonotot1  28071  usg2spthonot0  28086  usg2spthonot1  28087  2pthfrgra  28115  frgrancvvdeqlemC  28142  frgrawopreglem4  28150  onfrALTlem2  28343  2pm13.193  28350  onfrALTlem2VD  28710  lssats  29495  lfl0f  29552  ncvr1  29755  cvrletrN  29756  cvrnrefN  29765  iscvlat2N  29807  ltltncvr  29905  atcvrj2b  29914  atltcvr  29917  cvrat4  29925  islln3  29992  llnle  30000  2at0mat0  30007  islpln3  30015  islpln5  30017  islpln2a  30030  islvol3  30058  pmapglb2N  30253  pmapglb2xN  30254  isline3  30258  isline4N  30259  pmod1i  30330  pclbtwnN  30379  pclfinN  30382  pexmidN  30451  pexmidlem8N  30459  lhplt  30482  lhpexle1  30490  lhpjat1  30502  lhpj1  30504  lhpmcvr  30505  lhpmcvr2  30506  lhpm0atN  30511  lautcvr  30574  ldil1o  30594  ldilcnv  30597  ltrn1o  30606  idltrn  30632  cdlemc3  30675  cdlemc4  30676  cdlemd1  30680  cdleme0cp  30696  cdleme0cq  30697  cdlemeulpq  30702  cdleme1  30709  cdleme2  30710  cdleme3b  30711  cdleme3c  30712  cdlemedb  30779  cdleme27a  30849  cdlemefrs32fva  30882  cdleme42keg  30968  cdleme42mgN  30970  cdleme48gfv  31019  cdlemf2  31044  cdlemg1cex  31070  cdlemg5  31087  cdlemg4c  31094  trlcoat  31205  tgrpgrplem  31231  tendodi1  31266  tendodi2  31267  tendo0pl  31273  tendoicl  31278  tendoipl  31279  tendo0mul  31308  tendo0mulr  31309  dva1dim  31467  erngdvlem4  31473  erngdvlem4-rN  31481  tendospdi1  31503  dialss  31529  diaglbN  31538  diameetN  31539  dibglbN  31649  dib1dim2  31651  diblss  31653  dicssdvh  31669  diclss  31676  diclspsn  31677  dihlsscpre  31717  dihglblem5aN  31775  dihglblem4  31780  dihglblem5  31781  dih1dimatlem  31812  dihlsprn  31814  dihatlat  31817  dihglblem6  31823  dochvalr  31840
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
  Copyright terms: Public domain W3C validator