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  2655  rmob  3217  ifboth  3738  prneimg  3946  ordelord  4571  poinxp  4908  soltmin  5240  sofld  5285  f1oprswap  5684  mpteqb  5786  fvmptt  5787  iinpreima  5827  fcof1  5987  soisoi  6015  grprinvlem  6252  fnfvof  6284  dftpos4  6465  tfrlem9a  6614  oaass  6771  oelimcl  6810  nnawordex  6847  oaabs  6854  oaabs2  6855  omabs  6857  qsel  6950  th3qlem1  6977  mapss  7023  boxcutc  7072  omxpenlem  7176  xpmapenlem  7241  mapdom2  7245  unxpdomlem3  7282  f1finf1o  7302  frfi  7319  nnunifi  7325  indexfi  7380  elfi2  7385  elfiun  7401  marypha1lem  7404  supisolem  7439  ordtypelem7  7457  oismo  7473  wdomtr  7507  brwdom3  7514  cnfcomlem  7620  r1ordg  7668  rankval3b  7716  rankonidlem  7718  harcard  7829  infxpenlem  7859  acni2  7891  numacn  7894  fodomacn  7901  mappwen  7957  dfac9  7980  cdalepw  8040  infxpabs  8056  infunsdom1  8057  infunsdom  8058  ackbij1lem15  8078  cfsmolem  8114  infpssrlem5  8151  infpssr  8152  ssfin4  8154  fin2i2  8162  ssfin2  8164  fin23lem24  8166  fin23lem22  8171  fin23lem27  8172  fin23lem36  8192  isf32lem3  8199  isf32lem7  8203  isf34lem7  8223  fin1a2lem13  8256  hsmexlem4  8273  axdc4lem  8299  iundom2g  8379  alephexp1  8418  fpwwe2lem1  8470  fpwwe2lem8  8476  canthp1  8493  inttsk  8613  inar1  8614  r1tskina  8621  grur1  8659  nqerf  8771  distrlem1pr  8866  distrlem4pr  8867  reclem2pr  8889  addsub4  9308  le2add  9474  lt2sub  9490  le2sub  9491  mulge0  9509  receu  9631  rec11  9676  rec11r  9677  divdivdiv  9679  ddcan  9692  divadddiv  9693  divsubdiv  9694  conjmul  9695  rereccl  9696  subrec  9807  recgt0  9818  prodgt0  9819  prodge0  9821  ltmul12a  9830  lemul12a  9832  lemulge11  9836  lt2mul2div  9850  ltrec  9855  lerec  9856  lt2msq  9858  le2msq  9874  msq11  9875  ledivp1  9876  rimul  9955  zsupss  10529  uzwo3  10533  qreccl  10558  rpnnen1lem1  10564  rpnnen1lem2  10565  rpnnen1lem3  10566  rpnnen1lem5  10568  qbtwnre  10749  qbtwnxr  10750  xralrple  10755  xpncan  10794  xaddge0  10801  xle2add  10802  xmulneg1  10812  xmulgt0  10826  ixxss1  10898  ixxss2  10899  elioc2  10937  difreicc  10992  fzass4  11054  fzrev  11072  modid  11233  uzindi  11283  seqfeq3  11336  seqof2  11344  expcl2lem  11356  expnegz  11377  expadd  11385  expmul  11388  expcan  11395  ltexp2  11396  leexp1a  11401  expnlbnd  11472  digit1  11476  bcval5  11572  bcpasc  11575  hashprb  11631  fzsdom2  11656  hashbclem  11664  hashbc  11665  hashf1lem2  11668  seqcoll  11675  ccatswrd  11736  revccat  11761  sqrmul  12028  sqrlt  12030  sqrdiv  12034  absexpz  12073  abslt  12081  absle  12082  abssubne0  12083  rexico  12120  amgm2  12136  rlim3  12255  lo1bdd2  12281  climuni  12309  rlimcn1  12345  cn1lem  12354  iserex  12413  iserle  12416  isercolllem1  12421  climcau  12427  caucvgb  12436  iseralt  12441  summo  12474  zsum  12475  sumss2  12483  isumadd  12514  fsum2dlem  12517  fsum2d  12518  fsum0diag2  12529  fsumabs  12543  cvgcmp  12558  cvgcmpce  12560  incexclem  12579  incexc2  12581  isumsplit  12583  climcnds  12594  divrcnv  12595  geolim  12610  geo2lim  12615  geomulcvg  12616  mertenslem1  12624  mertenslem2  12625  mertens  12626  efcvgfsum  12651  eftlcl  12671  reeftlcl  12672  tanadd  12731  eirr  12767  rpnnen2  12788  sqr2irr  12811  dvds2ln  12843  dvdseq  12860  dvdsext  12863  bitsfzo  12910  sadadd2lem2  12925  sadadd  12942  bitsshft  12950  smupvallem  12958  smumul  12968  bezout  13005  gcdmultiplez  13014  dvdsmulgcd  13017  prmdvdsexp  13077  pcqmul  13190  pcexp  13196  pcneg  13210  pcdvdstr  13212  pcprmpw2  13218  pcfac  13231  expnprm  13234  prmpwdvds  13235  prmreclem6  13252  mul4sq  13285  vdwapf  13303  vdwlem13  13324  vdw  13325  vdwnnlem3  13328  vdwnn  13329  ramub2  13345  ramz  13356  ramcl  13360  ressress  13489  pwsle  13677  mreriincl  13786  mrcuni  13809  mreexexlemd  13832  isacs2  13841  acsfn  13847  acsfn1  13849  acsfn2  13851  iscat  13860  cidfval  13864  iscatd2  13869  monfval  13921  isfunc  14024  isfull2  14071  isfth2  14075  1stfval  14251  2ndfval  14254  yonedainv  14341  drsdirfi  14358  pospo  14393  mod1ile  14497  mod2ile  14498  isipodrs  14550  isacs4lem  14557  mrelatlub  14575  spwpr4  14626  submnd0  14688  resmhm  14722  mhmco  14725  mhmima  14726  pwsdiagmhm  14731  gsumwsubmcl  14747  gsumwmhm  14753  gsumwspan  14754  grprcan  14801  grplactcnv  14850  mulgz  14874  mulgnn0dir  14876  mulgdir  14878  mulgneg2  14880  mulgnn0ass  14882  mhmmulg  14885  pwssub  14894  pwsmulg  14895  issubg4  14924  nmzsubg  14944  ssnmz  14945  ghmmhmb  14980  resghm  14985  ghmpreima  14990  ghmnsgpreima  14993  ghmf1o  14998  isga  15031  gaid  15039  gass  15041  gapm  15046  gaorber  15048  gastacl  15049  gastacos  15050  lactghmga  15070  cntzsubm  15097  cntzsubg  15098  cntzmhm  15100  submod  15166  gexdvds  15181  gexcl3  15184  sylow2blem3  15219  lsmub1x  15243  lsmless12  15258  pj1id  15294  efglem  15311  efgcpbllemb  15350  mulgnn0di  15411  eqgabl  15417  gexex  15431  torsubg  15432  cygabl  15463  prmcyg  15466  cyggexb  15471  gsumval3  15477  subgdmdprd  15555  mgpress  15622  isrng  15631  rngpropd  15658  dvdsrtr  15720  isdrng2  15808  issubrg  15831  cntzsubr  15863  abvrec  15887  abvdiv  15888  islmodd  15919  lmodprop2d  15969  lssvsubcl  15983  lssvacl  15993  lssvscl  15994  islss3  15998  lss1d  16002  lsspropd  16056  islmhm  16066  lmhmco  16082  lmhmplusg  16083  lmhmf1o  16085  lmhmima  16086  lmhmpreima  16087  reslmhm  16091  lspextmo  16095  pwsdiaglmhm  16096  lmhmpropd  16108  islbs2  16189  lidlsubcl  16250  drngnidl  16263  2idlcpbl  16268  unitrrg  16316  fidomndrng  16330  issubassa  16346  assapropd  16349  psrbaglefi  16400  psrbagconf1o  16402  coe1mul2lem1  16623  ply1coe  16647  qsssubdrg  16721  cnsubrg  16722  zlpir  16734  domnchr  16776  znval  16779  znunit  16807  znrrg  16809  isphl  16822  ocvlss  16862  ocvin  16864  obslbs  16920  toponmre  17120  neissex  17154  clslp  17174  tgrest  17185  restcld  17198  ssrest  17202  restopn2  17203  pnfnei  17246  mnfnei  17247  cnpnei  17290  cnco  17292  cnss1  17302  cnss2  17303  isnrm2  17384  restcnrm  17388  dnsconst  17404  cmpsub  17425  uncmp  17428  dfcon2  17443  2ndcrest  17478  1stcelcls  17485  hausllycmp  17518  cldllycmp  17519  dislly  17521  kgencn  17549  ptpjpre2  17573  ptclsg  17608  dfac14  17611  txindis  17627  txlly  17629  txnlly  17630  txcmp  17636  xkoptsub  17647  xkopt  17648  xkoinjcn  17680  qtopkgen  17703  kqdisj  17725  kqcldsat  17726  isr0  17730  kqreglem2  17735  kqnrmlem2  17737  nrmr0reg  17742  reghmph  17786  nrmhmph  17787  infil  17856  fgabs  17872  filcon  17876  trfil2  17880  isufil2  17901  trufil  17903  filssufilg  17904  ssufl  17911  ufileu  17912  rnelfm  17946  fbflim  17969  flimclsi  17971  flimsncls  17979  hauspwpwf1  17980  fclsval  18001  fclscf  18018  flimfnfcls  18021  uffclsflim  18024  alexsubb  18038  cnextcn  18059  tmdmulg  18083  symgtgp  18092  utoptop  18225  utopsnneiplem  18238  psmetres2  18306  xmetres2  18352  xblss2ps  18392  blhalf  18396  blssexps  18417  blssex  18418  blin2  18420  blbas  18421  met1stc  18512  met2ndci  18513  metcnpi  18535  metcnpi2  18536  metusttoOLD  18548  metustto  18549  metustexhalfOLD  18554  metustexhalf  18555  elbl4  18567  metuel2  18570  dscopn  18582  ngpinvds  18620  subgngp  18637  tngngp  18656  nmdvr  18667  nlmvscn  18684  nrginvrcn  18688  lssnlm  18697  nmoco  18732  blcvx  18790  tgqioo  18792  icccmplem2  18815  metdstri  18842  metdsle  18843  metdsre  18844  cncfss  18890  icoopnst  18925  phtpycc  18977  phtpc01  18982  pcohtpylem  19005  clmmulg  19079  iscph  19094  ipcn  19161  csscld  19164  clsocv  19165  cfilfcls  19188  cmetcau  19203  iscmet3lem2  19206  lmclim  19216  flimcfil  19227  cmetss  19228  bcth  19243  bcth2  19244  cmetcuspOLD  19268  cmetcusp  19269  ivthicc  19316  ovolficc  19326  ovolctb  19347  ovolun  19356  ovolfiniun  19358  ovoliunlem2  19360  ovoliunlem3  19361  ovolicc2lem3  19376  ovolicc2lem4  19377  unmbl  19393  shftmbl  19394  volfiniun  19402  voliunlem3  19407  volsup  19411  ioombl  19420  volcn  19459  volivth  19460  vitalilem1  19461  mbfconstlem  19482  mbfposr  19505  cnmbf  19512  mbflimsup  19519  i1fd  19534  i1f1  19543  itg10a  19563  itg2le  19592  itg2const2  19594  iblss  19657  itgeqa  19666  bddmulibl  19691  cnplimc  19735  limccnp2  19740  dvres  19759  dvnres  19778  dvcj  19797  dvrec  19802  dvmptfsum  19820  dvexp3  19823  dveflem  19824  dvfsumrlimge0  19875  evlsval  19901  tdeglem4  19944  ply1domn  20007  elply2  20076  ply1termlem  20083  plypf1  20092  plymullem1  20094  dgrlem  20109  coeid  20118  coeeq2  20122  coemulc  20134  dgreq0  20144  dvply2g  20163  plydivalg  20177  plyexmo  20191  elqaa  20200  aaliou3lem8  20223  dvtaylp  20247  mtest  20281  abelthlem2  20309  ptolemy  20365  cosord  20395  logdivle  20478  divlogrlim  20487  logcnlem5  20498  logtayl  20512  cxpmul2  20541  abscxp2  20545  cxplt  20546  cxple  20547  cxplt3  20552  atantayl3  20740  birthdaylem3  20753  rlimcnp2  20766  efrlim  20769  cxploglim2  20778  scvxcvx  20785  fta  20823  efnnfsumcl  20846  isppw2  20859  sqf11  20883  sgmval  20886  sgmval2  20887  efchtdvds  20903  sqff1o  20926  sgmmul  20946  pclogsum  20960  vmasum  20961  logfac2  20962  logexprlim  20970  perfect  20976  dchrelbas4  20988  dchrptlem2  21010  bcmax  21023  bposlem1  21029  bpos  21038  lgslem4  21044  lgsdir2lem5  21072  2sqlem6  21114  dchrisumlem3  21146  dchrmusum2  21149  pntrlog2bnd  21239  pntlem3  21264  pnt3  21267  qabvexp  21281  ostth  21294  umgra1  21322  uslgra1  21353  usgra1  21354  usgraedg4  21367  wlkres  21490  wlkbprop  21495  0pthon  21540  constr2trl  21560  crcts  21570  cycls  21571  constr3trllem5  21602  constr3cycllem1  21606  constr3cyclp  21610  3v3e3cycl  21613  4cycl4v4e  21614  4cycl4dv4e  21616  eupatrl  21651  grpoidinvlem4  21756  grpoideu  21758  grpoidinv2  21767  rngo2  21937  blocnilem  22266  ipblnfi  22318  minvecolem4  22343  hvmul0or  22488  his35  22551  pjhtheu2  22879  3oalem2  23126  bralnfn  23412  kbpj  23420  eighmorth  23428  hmopm  23485  hmopco  23487  lnconi  23497  riesz3i  23526  cnlnadjlem6  23536  adjmul  23556  leopmuli  23597  nmopleid  23603  dmdbr2  23767  mdslmd1lem1  23789  superpos  23818  chirredlem2  23855  chirredi  23858  atcvat4i  23861  ifeqeqx  23962  iuninc  23972  abfmpeld  24027  xaddeq0  24080  xreceu  24129  toslub  24152  tosglb  24153  xrsmulgzz  24161  gsumpropd2lem  24181  ofldsqr  24201  ofldchr  24205  pstmxmet  24253  xpinpreima2  24266  sqsscirc2  24268  xrge0iifiso  24282  elzrhunit  24324  qqhf  24331  qqhucn  24337  indpreima  24383  indf1ofs  24384  gsumesum  24412  esumlub  24413  esumpr2  24419  esumfzf  24420  esumfsup  24421  esumpcvgval  24429  esumcvg  24437  sigainb  24480  insiga  24481  measiuns  24532  meascnbl  24534  measinb  24536  measdivcstOLD  24539  measdivcst  24540  dya2iocnrect  24592  dya2iocnei  24593  dya2iocucvr  24595  sibfof  24615  ballotlemfc0  24711  ballotlemfcc  24712  ballotlemsima  24734  gamcvg2lem  24804  subfacp1lem6  24832  pconcon  24879  conpcon  24883  sconpi1  24887  txscon  24889  cnllyscon  24893  cvmopnlem  24926  cvmfolem  24927  cvmlift  24947  sinccvg  25071  relexp0  25090  relexpindlem  25100  divelunit  25146  mulge0b  25152  ntrivcvgmullem  25190  prodmolem2  25222  prodmo  25223  zprod  25224  fprod2dlem  25265  risefallfac  25300  fallfacfwd  25311  sltval2  25532  nodense  25565  nofulllem4  25581  colinearalglem4  25760  axcontlem2  25816  axcontlem4  25818  axcontlem7  25821  axcontlem8  25822  axcontlem9  25823  axcontlem10  25824  btwncomim  25859  btwnswapid  25863  lineext  25922  btwnconn1lem11  25943  btwnconn1lem14  25946  broutsideof3  25972  outsideoftr  25975  outsidele  25978  ellines  25998  linethru  25999  lxflflp1  26150  mblfinlem  26151  mblfinlem2  26152  ismblfin  26154  itg2addnclem  26163  itg2addnclem2  26164  itg2addnc  26166  locfindis  26283  neibastop2lem  26287  neibastop2  26288  sdclem1  26345  geomcau  26363  isbnd3  26391  prdsbnd2  26402  ismtyhmeo  26412  heibor1  26417  rrnmet  26436  rrndstprj1  26437  rrncmslem  26439  rrncms  26440  iccbnd  26447  prter3  26629  elrfirn2  26648  mrefg3  26660  isnacs3  26662  mzprename  26704  rexrabdioph  26752  icodiamlt  26781  pellexlem3  26792  pellex  26796  pellqrex  26840  pellfundex  26847  pellfund14b  26860  monotoddzzfi  26903  rpexpmord  26909  jm2.24  26926  congsym  26931  acongtr  26941  bezoutr  26948  bezoutr1  26949  jm2.18  26957  harinf  27003  kelac1  27037  lnmlsslnm  27055  dsmmbas2  27079  dsmmfi  27080  frlmlbs  27125  isnumbasgrplem3  27146  lindfind  27162  lindfrn  27167  islindf3  27172  hbt  27210  dgraalem  27226  mpaaeu  27231  f1omvdconj  27265  pmtrfinv  27278  symggen  27287  psgnunilem3  27295  grpvrinv  27327  matrng  27356  matassa  27357  mat1  27358  mendlmod  27377  acsfn1p  27383  proot1mul  27391  ofmul12  27418  ofdivdiv2  27421  refsumcn  27576  fmul01lt1lem1  27589  climsuselem1  27608  climsuse  27609  stoweidlem7  27631  stoweidlem14  27638  stoweidlem19  27643  stoweidlem20  27644  stoweidlem26  27650  stoweidlem31  27655  stoweidlem34  27658  stoweidlem39  27663  stoweidlem44  27668  stoweidlem46  27670  stoweidlem48  27672  stoweidlem59  27683  stoweidlem60  27684  stirlinglem5  27702  afvco2  27915  ndmaovdistr  27946  2f1fvneq  27966  imarnf1pr  27973  hashimarn  28002  swrdccatin12lem3a  28029  swrdccatin12lem3  28032  swrdccatin12b  28035  usgra2pthspth  28043  el2wlkonotot1  28079  usg2spthonot0  28094  usg2spthonot1  28095  2pthfrgra  28123  frgrancvvdeqlemC  28150  frgrawopreglem4  28158  onfrALTlem2  28351  2pm13.193  28358  onfrALTlem2VD  28719  lssats  29507  lfl0f  29564  ncvr1  29767  cvrletrN  29768  cvrnrefN  29777  iscvlat2N  29819  ltltncvr  29917  atcvrj2b  29926  atltcvr  29929  cvrat4  29937  islln3  30004  llnle  30012  2at0mat0  30019  islpln3  30027  islpln5  30029  islpln2a  30042  islvol3  30070  pmapglb2N  30265  pmapglb2xN  30266  isline3  30270  isline4N  30271  pmod1i  30342  pclbtwnN  30391  pclfinN  30394  pexmidN  30463  pexmidlem8N  30471  lhplt  30494  lhpexle1  30502  lhpjat1  30514  lhpj1  30516  lhpmcvr  30517  lhpmcvr2  30518  lhpm0atN  30523  lautcvr  30586  ldil1o  30606  ldilcnv  30609  ltrn1o  30618  idltrn  30644  cdlemc3  30687  cdlemc4  30688  cdlemd1  30692  cdleme0cp  30708  cdleme0cq  30709  cdlemeulpq  30714  cdleme1  30721  cdleme2  30722  cdleme3b  30723  cdleme3c  30724  cdlemedb  30791  cdleme27a  30861  cdlemefrs32fva  30894  cdleme42keg  30980  cdleme42mgN  30982  cdleme48gfv  31031  cdlemf2  31056  cdlemg1cex  31082  cdlemg5  31099  cdlemg4c  31106  trlcoat  31217  tgrpgrplem  31243  tendodi1  31278  tendodi2  31279  tendo0pl  31285  tendoicl  31290  tendoipl  31291  tendo0mul  31320  tendo0mulr  31321  dva1dim  31479  erngdvlem4  31485  erngdvlem4-rN  31493  tendospdi1  31515  dialss  31541  diaglbN  31550  diameetN  31551  dibglbN  31661  dib1dim2  31663  diblss  31665  dicssdvh  31681  diclss  31688  diclspsn  31689  dihlsscpre  31729  dihglblem5aN  31787  dihglblem4  31792  dihglblem5  31793  dih1dimatlem  31824  dihlsprn  31826  dihatlat  31829  dihglblem6  31835  dochvalr  31852
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