MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simpll 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 6    /\ wa 360
This theorem is referenced by:  simp1ll  1020  simp2ll  1024  simp3ll  1028  pm2.61da3ne  2527  rmob  3080  ifboth  3597  ordelord  4413  poinxp  4752  soltmin  5081  sofld  5120  f1oprswap  5480  mpteqb  5575  fvmptt  5576  iinpreima  5616  fcof1  5758  soisoi  5786  grprinvlem  6019  fnfvof  6051  dftpos4  6214  tfrlem9a  6397  oaass  6554  oelimcl  6593  nnawordex  6630  oaabs  6637  oaabs2  6638  omabs  6640  qsel  6733  th3qlem1  6759  mapss  6805  boxcutc  6854  omxpenlem  6958  xpmapenlem  7023  mapdom2  7027  unxpdomlem3  7064  f1finf1o  7081  frfi  7097  nnunifi  7103  indexfi  7158  elfi2  7163  elfiun  7178  marypha1lem  7181  supisolem  7216  ordtypelem7  7234  oismo  7250  wdomtr  7284  brwdom3  7291  cnfcomlem  7397  r1ordg  7445  rankval3b  7493  rankonidlem  7495  harcard  7606  infxpenlem  7636  acni2  7668  numacn  7671  acndom2  7676  fodomacn  7678  mappwen  7734  dfac9  7757  cdalepw  7817  infxpabs  7833  infunsdom1  7834  infunsdom  7835  ackbij1lem15  7855  cfsmolem  7891  infpssrlem5  7928  infpssr  7929  ssfin4  7931  fin2i2  7939  ssfin2  7941  fin23lem24  7943  fin23lem22  7948  fin23lem27  7949  fin23lem36  7969  isf32lem3  7976  isf32lem7  7980  isf34lem7  8000  fin1a2lem13  8033  hsmexlem4  8050  axdc4lem  8076  ttukeylem6  8136  iundom2g  8157  alephexp1  8196  fpwwe2lem1  8248  fpwwe2lem8  8254  fpwwe2lem12  8258  canthp1  8271  inttsk  8391  inar1  8392  r1tskina  8399  grur1  8437  nqerf  8549  distrlem1pr  8644  distrlem4pr  8645  reclem2pr  8667  addsub4  9085  le2add  9251  lt2sub  9267  le2sub  9268  mulge0  9286  receu  9408  rec11  9453  rec11r  9454  divdivdiv  9456  ddcan  9469  divadddiv  9470  divsubdiv  9471  conjmul  9472  rereccl  9473  subrec  9584  recgt0  9595  prodgt0  9596  prodge0  9598  ltmul12a  9607  lemul12a  9609  lemulge11  9613  lt2mul2div  9627  ltrec  9632  lerec  9633  lt2msq  9635  le2msq  9651  msq11  9652  ledivp1  9653  rimul  9732  zsupss  10302  uzwo3  10306  qreccl  10331  rpnnen1lem1  10337  rpnnen1lem2  10338  rpnnen1lem3  10339  rpnnen1lem5  10341  qbtwnre  10520  qbtwnxr  10521  xralrple  10526  xpncan  10565  xaddge0  10572  xle2add  10573  xmulneg1  10583  xmulgt0  10597  ixxss1  10668  ixxss2  10669  elioc2  10707  difreicc  10761  fzass4  10823  fzrev  10840  modid  10987  uzindi  11037  seqfeq3  11090  expcl2lem  11109  expnegz  11130  expadd  11138  expmul  11141  expcan  11148  ltexp2  11149  leexp1a  11154  expnlbnd  11225  digit1  11229  bcval5  11324  bcpasc  11327  fzsdom2  11376  hashbclem  11384  hashbc  11385  hashf1lem2  11388  seqcoll  11395  ccatswrd  11453  revccat  11478  sqrmul  11739  sqrlt  11741  sqrdiv  11745  absexpz  11784  abslt  11792  absle  11793  abssubne0  11794  rexico  11831  amgm2  11847  rlim3  11966  lo1bdd2  11992  climuni  12020  rlimcn1  12056  cn1lem  12065  iserex  12124  iserle  12127  isercolllem1  12132  climcau  12138  caucvgb  12146  iseralt  12151  summo  12184  zsum  12185  sumss2  12193  isumadd  12224  fsum2dlem  12227  fsum2d  12228  fsum0diag2  12239  fsumabs  12253  cvgcmp  12268  cvgcmpce  12270  incexclem  12289  incexc2  12291  isumsplit  12293  climcnds  12304  divrcnv  12305  geolim  12320  geo2lim  12325  geomulcvg  12326  mertenslem1  12334  mertenslem2  12335  mertens  12336  efcvgfsum  12361  eftlcl  12381  reeftlcl  12382  tanadd  12441  eirr  12477  rpnnen2  12498  sqr2irr  12521  dvds2ln  12553  dvdseq  12570  dvdsext  12573  bitsfzo  12620  sadadd2lem2  12635  sadadd  12652  bitsshft  12660  smupvallem  12668  smumul  12678  bezout  12715  gcdmultiplez  12724  dvdsmulgcd  12727  prmdvdsexp  12787  pcqmul  12900  pcexp  12906  pcneg  12920  pcdvdstr  12922  pcprmpw2  12928  pcfac  12941  expnprm  12944  prmpwdvds  12945  prmreclem6  12962  mul4sq  12995  vdwapf  13013  vdwlem13  13034  vdw  13035  vdwnnlem3  13038  vdwnn  13039  ramub2  13055  ramz  13066  ramcl  13070  ressress  13199  pwsle  13385  mreriincl  13494  mrcuni  13517  mreexexlemd  13540  isacs2  13549  acsfn  13555  acsfn1  13557  acsfn2  13559  iscat  13568  cidfval  13572  iscatd2  13577  monfval  13629  isfunc  13732  isfull2  13779  isfth2  13783  1stfval  13959  2ndfval  13962  yonedainv  14049  drsdirfi  14066  pospo  14101  mod1ile  14205  mod2ile  14206  isipodrs  14258  isacs4lem  14265  mrelatlub  14283  spwpr4  14334  submnd0  14396  resmhm  14430  mhmco  14433  mhmima  14434  pwsdiagmhm  14439  gsumwsubmcl  14455  gsumwmhm  14461  gsumwspan  14462  grprcan  14509  grplactcnv  14558  mulgz  14582  mulgnn0dir  14584  mulgdir  14586  mulgneg2  14588  mulgnn0ass  14590  mhmmulg  14593  pwssub  14602  pwsmulg  14603  issubg4  14632  nmzsubg  14652  ssnmz  14653  ghmmhmb  14688  resghm  14693  ghmpreima  14698  ghmnsgpreima  14701  ghmf1o  14706  isga  14739  gaid  14747  gass  14749  gapm  14754  gaorber  14756  gastacl  14757  gastacos  14758  lactghmga  14778  cntzsubm  14805  cntzsubg  14806  cntzmhm  14808  dfod2  14871  submod  14874  gexdvds  14889  gexcl3  14892  pgpfi  14910  sylow2blem3  14927  lsmub1x  14951  lsmless12  14966  pj1id  15002  efglem  15019  efgcpbllemb  15058  mulgnn0di  15119  eqgabl  15125  gexex  15139  torsubg  15140  cygabl  15171  prmcyg  15174  ghmcyg  15176  cyggexb  15179  gsumval3  15185  subgdmdprd  15263  mgpress  15330  isrng  15339  rngpropd  15366  dvdsrtr  15428  isdrng2  15516  issubrg  15539  cntzsubr  15571  abvrec  15595  abvdiv  15596  islmodd  15627  lmodprop2d  15681  lssvsubcl  15695  lssvacl  15705  lssvscl  15706  islss3  15710  lss1d  15714  lsspropd  15768  islmhm  15778  lmhmco  15794  lmhmplusg  15795  lmhmf1o  15797  lmhmima  15798  lmhmpreima  15799  reslmhm  15803  lspextmo  15807  pwsdiaglmhm  15808  lmhmpropd  15820  islbs2  15901  lidlsubcl  15962  drngnidl  15975  2idlcpbl  15980  unitrrg  16028  fidomndrng  16042  issubassa  16058  assapropd  16061  psrbaglefi  16112  psrbagconf1o  16114  coe1mul2lem1  16338  ply1coe  16362  qsssubdrg  16425  cnsubrg  16426  zlpir  16438  domnchr  16480  znval  16483  znunit  16511  znrrg  16513  isphl  16526  ocvlss  16566  ocvin  16568  obslbs  16624  toponmre  16824  neissex  16858  clslp  16873  tgrest  16884  restcld  16897  ssrest  16901  restopn2  16902  pnfnei  16944  mnfnei  16945  cnpnei  16987  cnco  16989  cnss1  16999  cnss2  17000  cncnp  17003  isnrm2  17080  restcnrm  17084  dnsconst  17100  cmpsub  17121  uncmp  17124  dfcon2  17139  2ndcrest  17174  1stcelcls  17181  subislly  17201  hausllycmp  17214  cldllycmp  17215  dislly  17217  kgencn  17245  ptpjpre2  17269  ptclsg  17303  dfac14  17306  ptcnplem  17309  txindis  17322  txlly  17324  txnlly  17325  pthaus  17326  txcmp  17331  xkohaus  17341  xkoptsub  17342  xkopt  17343  xkoinjcn  17375  qtopkgen  17395  kqdisj  17417  kqcldsat  17418  isr0  17422  kqreglem2  17427  kqnrmlem2  17429  nrmr0reg  17434  reghmph  17478  nrmhmph  17479  infil  17552  fgabs  17568  filcon  17572  trfil2  17576  isufil2  17597  trufil  17599  filssufilg  17600  ssufl  17607  ufileu  17608  rnelfm  17642  fbflim  17665  flimclsi  17667  flimsncls  17675  hauspwpwf1  17676  fclsval  17697  fclscf  17714  flimfnfcls  17717  uffclsflim  17720  alexsubb  17734  tmdmulg  17769  symgtgp  17778  xmetres2  17919  blhalf  17954  blssex  17967  blin2  17969  blbas  17970  met1stc  18061  met2ndci  18062  metcnpi  18084  metcnpi2  18085  dscopn  18090  ngpinvds  18128  subgngp  18145  tngngp  18164  nmdvr  18175  nlmvscn  18192  nrginvrcn  18196  lssnlm  18205  nmoco  18240  blcvx  18298  tgqioo  18300  icccmplem2  18322  xrge0tsms  18333  metdstri  18349  metdsle  18350  metdsre  18351  cncfss  18397  icoopnst  18431  phtpycc  18483  phtpc01  18488  pcohtpylem  18511  clmmulg  18585  nmoleub2lem2  18591  iscph  18600  ipcn  18667  csscld  18670  clsocv  18671  cfilfcls  18694  cmetcau  18709  iscmet3lem2  18712  lmclim  18722  flimcfil  18733  cmetss  18734  bcth  18745  bcth2  18746  ivthicc  18812  ovolficc  18822  ovolctb  18843  ovolun  18852  ovolfiniun  18854  ovoliunlem2  18856  ovoliunlem3  18857  ovolicc2lem3  18872  ovolicc2lem4  18873  unmbl  18889  shftmbl  18890  volfiniun  18898  voliunlem3  18903  volsup  18907  ioombl  18916  volcn  18955  volivth  18956  vitalilem1  18957  mbfconstlem  18978  mbfposr  19001  cnmbf  19008  mbflimsup  19015  i1fd  19030  i1f1  19039  itg10a  19059  itg2le  19088  itg2const2  19090  iblss  19153  itgeqa  19162  bddmulibl  19187  cnplimc  19231  limccnp2  19236  dvres  19255  dvnres  19274  dvcj  19293  dvrec  19298  dvmptfsum  19316  dvexp3  19319  dveflem  19320  dvlip2  19336  dvfsumrlimge0  19371  evlsval  19397  tdeglem4  19440  ply1domn  19503  elply2  19572  ply1termlem  19579  plypf1  19588  plymullem1  19590  dgrlem  19605  coeid  19614  coeeq2  19618  coemulc  19630  dgreq0  19640  dvply2g  19659  plydivalg  19673  plyexmo  19687  elqaa  19696  aaliou3lem8  19719  dvtaylp  19743  ulm2  19758  mtest  19775  abelthlem2  19802  ptolemy  19858  cosord  19888  logdivle  19967  divlogrlim  19976  logcnlem5  19987  efopn  19999  logtayl  20001  cxpmul2  20030  abscxp2  20034  cxplt  20035  cxple  20036  cxplt3  20041  atantayl3  20229  birthdaylem3  20242  rlimcnp2  20255  efrlim  20258  cxploglim2  20267  scvxcvx  20274  fta  20311  efnnfsumcl  20334  isppw2  20347  sqf11  20371  sgmval  20374  sgmval2  20375  efchtdvds  20391  sqff1o  20414  sgmmul  20434  pclogsum  20448  vmasum  20449  logfac2  20450  logexprlim  20458  perfect  20464  dchrelbas4  20476  dchrptlem2  20498  bcmax  20511  bposlem1  20517  bpos  20526  lgslem4  20532  lgsdir2lem5  20560  2sqlem6  20602  dchrisumlem3  20634  dchrmusum2  20637  pntrlog2bnd  20727  pntibnd  20736  pntlem3  20752  pnt3  20755  qabvexp  20769  ostth  20782  grpoidinvlem4  20866  grpoideu  20868  grpoidinv2  20877  rngo2  21047  blocnilem  21374  ipblnfi  21426  minvecolem4  21451  hvmul0or  21596  his35  21659  pjhtheu2  21987  3oalem2  22234  bralnfn  22520  kbpj  22528  eighmorth  22536  hmopm  22593  hmopco  22595  lnconi  22605  riesz3i  22634  cnlnadjlem6  22644  adjmul  22664  leopmuli  22705  nmopleid  22711  dmdbr2  22875  mdslmd1lem1  22897  superpos  22926  chirredlem2  22963  chirredi  22966  atcvat4i  22969  ifeqeqx  23026  ballotlemfc0  23044  ballotlemfcc  23045  ballotlemsima  23067  subfacp1lem6  23120  pconcon  23166  conpcon  23170  sconpi1  23174  txscon  23176  cnllyscon  23180  cvmopnlem  23213  cvmfolem  23214  cvmlift  23234  umgra1  23282  sinccvg  23410  relexp0  23429  relexpindlem  23440  divelunit  23483  mulge0b  23489  sltval2  23710  axdense  23744  axfelem20  23766  colinearalglem4  23944  axcontlem2  24000  axcontlem4  24002  axcontlem7  24005  axcontlem8  24006  axcontlem9  24007  axcontlem10  24008  btwncomim  24043  btwnswapid  24047  lineext  24106  btwnconn1lem11  24127  btwnconn1lem14  24130  broutsideof3  24156  outsideoftr  24159  outsidele  24162  ellines  24182  linethru  24183  cbicp  24565  geme2  24674  ranncnt  24682  trran2  24792  ltrran2  24802  ltrinvlem  24805  osneisi  24930  qusp  24941  cnpflf4  24963  limptlimpr2lem1  24973  iintlem1  25009  flfneicn  25024  addcanrg  25066  subaddv  25070  distmlva  25087  icccon3  25100  icmpmon  25215  iepiclem  25222  locfindis  25704  neibastop2lem  25708  neibastop2  25709  sdclem1  25852  geomcau  25874  isbnd3  25907  prdstotbnd  25917  prdsbnd2  25918  ismtyhmeo  25928  heibor1  25933  rrnmet  25952  rrndstprj1  25953  rrncmslem  25955  rrncms  25956  iccbnd  25963  prter3  26149  elrfirn2  26170  mrefg3  26182  isnacs3  26184  mzprename  26226  eldioph2  26240  rexrabdioph  26274  rencldnfilem  26302  icodiamlt  26304  pellexlem3  26315  pellex  26319  pell14qrdich  26353  pellqrex  26363  pellfundex  26370  pellfund14b  26383  monotoddzzfi  26426  rpexpmord  26432  jm2.24  26449  congsym  26454  acongtr  26464  dvdsacongtr  26470  bezoutr  26471  bezoutr1  26472  jm2.18  26480  harinf  26526  kelac1  26560  lnmlsslnm  26578  dsmmbas2  26602  dsmmfi  26603  frlmlbs  26648  isnumbasgrplem3  26669  lindfind  26685  lindfrn  26690  islindf3  26695  hbt  26733  dgraalem  26749  mpaaeu  26754  f1omvdconj  26788  pmtrfinv  26801  symggen  26810  psgnunilem3  26818  grpvrinv  26850  matrng  26879  matassa  26880  mat1  26881  mendlmod  26900  acsfn1p  26906  proot1mul  26914  ofmul12  26941  ofdivdiv2  26944  fnchoice  27099  refsumcn  27100  fmuldfeq  27112  fmul01lt1lem1  27113  climsuselem1  27132  climsuse  27133  stoweidlem7  27155  stoweidlem14  27162  stoweidlem19  27167  stoweidlem20  27168  stoweidlem26  27174  stoweidlem27  27175  stoweidlem30  27178  stoweidlem31  27179  stoweidlem34  27182  stoweidlem35  27183  stoweidlem38  27186  stoweidlem39  27187  stoweidlem43  27191  stoweidlem44  27192  stoweidlem46  27194  stoweidlem48  27196  stoweidlem49  27197  stoweidlem52  27200  stoweidlem53  27201  stoweidlem54  27202  stoweidlem55  27203  stoweidlem56  27204  stoweidlem57  27205  stoweidlem58  27206  stoweidlem59  27207  stoweidlem60  27208  stoweidlem61  27209  stoweidlem62  27210  stoweid  27211  stirlinglem5  27226  afvco2  27414  ndmaovdistr  27446  onfrALTlem2  27582  2pm13.193  27589  onfrALTlem2VD  27933  lssats  28469  lfl0f  28526  ncvr1  28729  cvrletrN  28730  cvrnrefN  28739  iscvlat2N  28781  ltltncvr  28879  atcvrj2b  28888  atltcvr  28891  cvrat4  28899  islln3  28966  llnle  28974  2at0mat0  28981  islpln3  28989  islpln5  28991  islpln2a  29004  islvol3  29032  pmapglb2N  29227  pmapglb2xN  29228  isline3  29232  isline4N  29233  pmod1i  29304  pclbtwnN  29353  pclfinN  29356  pexmidN  29425  pexmidlem8N  29433  lhplt  29456  lhpexle1  29464  lhpjat1  29476  lhpj1  29478  lhpmcvr  29479  lhpmcvr2  29480  lhpm0atN  29485  lautcvr  29548  ldil1o  29568  ldilcnv  29571  ltrn1o  29580  ltrnid  29591  idltrn  29606  cdlemc3  29649  cdlemc4  29650  cdlemd1  29654  cdleme0cp  29670  cdleme0cq  29671  cdlemeulpq  29676  cdleme1  29683  cdleme2  29684  cdleme3b  29685  cdleme3c  29686  cdlemedb  29753  cdleme27a  29823  cdlemefrs32fva  29856  cdleme42keg  29942  cdleme42mgN  29944  cdleme48gfv  29993  cdlemf2  30018  cdlemg1a  30026  cdlemg1cex  30044  cdlemg5  30061  cdlemg4c  30068  trlcoat  30179  tgrpgrplem  30205  tendodi1  30240  tendodi2  30241  tendo0pl  30247  tendoicl  30252  tendoipl  30253  tendo0mul  30282  tendo0mulr  30283  dva1dim  30441  erngdvlem4  30447  erngdvlem4-rN  30455  tendospdi1  30477  dialss  30503  diaglbN  30512  diameetN  30513  dibglbN  30623  dib1dim2  30625  diblss  30627  dicssdvh  30643  diclss  30650  diclspsn  30651  dihlsscpre  30691  dihglblem5aN  30749  dihglblem4  30754  dihglblem5  30755  dih1dimatlem  30786  dihlsprn  30788  dihatlat  30791  dihglblem6  30797  dochvalr  30814
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator