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

Theorem simpll 730
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 19 . 2  |-  ( ph  ->  ph )
21ad2antrr 706 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  simp1ll  1018  simp2ll  1022  simp3ll  1026  pm2.61da3ne  2559  rmob  3113  ifboth  3630  ordelord  4451  poinxp  4790  soltmin  5119  sofld  5158  f1oprswap  5553  mpteqb  5652  fvmptt  5653  iinpreima  5693  fcof1  5839  soisoi  5867  grprinvlem  6100  fnfvof  6132  dftpos4  6295  tfrlem9a  6444  oaass  6601  oelimcl  6640  nnawordex  6677  oaabs  6684  oaabs2  6685  omabs  6687  qsel  6780  th3qlem1  6807  mapss  6853  boxcutc  6902  omxpenlem  7006  xpmapenlem  7071  mapdom2  7075  unxpdomlem3  7112  f1finf1o  7131  frfi  7147  nnunifi  7153  indexfi  7208  elfi2  7213  elfiun  7228  marypha1lem  7231  supisolem  7266  ordtypelem7  7284  oismo  7300  wdomtr  7334  brwdom3  7341  cnfcomlem  7447  r1ordg  7495  rankval3b  7543  rankonidlem  7545  harcard  7656  infxpenlem  7686  acni2  7718  numacn  7721  acndom2  7726  fodomacn  7728  mappwen  7784  dfac9  7807  cdalepw  7867  infxpabs  7883  infunsdom1  7884  infunsdom  7885  ackbij1lem15  7905  cfsmolem  7941  infpssrlem5  7978  infpssr  7979  ssfin4  7981  fin2i2  7989  ssfin2  7991  fin23lem24  7993  fin23lem22  7998  fin23lem27  7999  fin23lem36  8019  isf32lem3  8026  isf32lem7  8030  isf34lem7  8050  fin1a2lem13  8083  hsmexlem4  8100  axdc4lem  8126  ttukeylem6  8186  iundom2g  8207  alephexp1  8246  fpwwe2lem1  8298  fpwwe2lem8  8304  fpwwe2lem12  8308  canthp1  8321  inttsk  8441  inar1  8442  r1tskina  8449  grur1  8487  nqerf  8599  distrlem1pr  8694  distrlem4pr  8695  reclem2pr  8717  addsub4  9135  le2add  9301  lt2sub  9317  le2sub  9318  mulge0  9336  receu  9458  rec11  9503  rec11r  9504  divdivdiv  9506  ddcan  9519  divadddiv  9520  divsubdiv  9521  conjmul  9522  rereccl  9523  subrec  9634  recgt0  9645  prodgt0  9646  prodge0  9648  ltmul12a  9657  lemul12a  9659  lemulge11  9663  lt2mul2div  9677  ltrec  9682  lerec  9683  lt2msq  9685  le2msq  9701  msq11  9702  ledivp1  9703  rimul  9782  zsupss  10354  uzwo3  10358  qreccl  10383  rpnnen1lem1  10389  rpnnen1lem2  10390  rpnnen1lem3  10391  rpnnen1lem5  10393  qbtwnre  10573  qbtwnxr  10574  xralrple  10579  xpncan  10618  xaddge0  10625  xle2add  10626  xmulneg1  10636  xmulgt0  10650  ixxss1  10721  ixxss2  10722  elioc2  10760  difreicc  10814  fzass4  10876  fzrev  10893  modid  11040  uzindi  11090  seqfeq3  11143  expcl2lem  11162  expnegz  11183  expadd  11191  expmul  11194  expcan  11201  ltexp2  11202  leexp1a  11207  expnlbnd  11278  digit1  11282  bcval5  11377  bcpasc  11380  fzsdom2  11429  hashbclem  11437  hashbc  11438  hashf1lem2  11441  seqcoll  11448  ccatswrd  11506  revccat  11531  sqrmul  11792  sqrlt  11794  sqrdiv  11798  absexpz  11837  abslt  11845  absle  11846  abssubne0  11847  rexico  11884  amgm2  11900  rlim3  12019  lo1bdd2  12045  climuni  12073  rlimcn1  12109  cn1lem  12118  iserex  12177  iserle  12180  isercolllem1  12185  climcau  12191  caucvgb  12199  iseralt  12204  summo  12237  zsum  12238  sumss2  12246  isumadd  12277  fsum2dlem  12280  fsum2d  12281  fsum0diag2  12292  fsumabs  12306  cvgcmp  12321  cvgcmpce  12323  incexclem  12342  incexc2  12344  isumsplit  12346  climcnds  12357  divrcnv  12358  geolim  12373  geo2lim  12378  geomulcvg  12379  mertenslem1  12387  mertenslem2  12388  mertens  12389  efcvgfsum  12414  eftlcl  12434  reeftlcl  12435  tanadd  12494  eirr  12530  rpnnen2  12551  sqr2irr  12574  dvds2ln  12606  dvdseq  12623  dvdsext  12626  bitsfzo  12673  sadadd2lem2  12688  sadadd  12705  bitsshft  12713  smupvallem  12721  smumul  12731  bezout  12768  gcdmultiplez  12777  dvdsmulgcd  12780  prmdvdsexp  12840  pcqmul  12953  pcexp  12959  pcneg  12973  pcdvdstr  12975  pcprmpw2  12981  pcfac  12994  expnprm  12997  prmpwdvds  12998  prmreclem6  13015  mul4sq  13048  vdwapf  13066  vdwlem13  13087  vdw  13088  vdwnnlem3  13091  vdwnn  13092  ramub2  13108  ramz  13119  ramcl  13123  ressress  13252  pwsle  13440  mreriincl  13549  mrcuni  13572  mreexexlemd  13595  isacs2  13604  acsfn  13610  acsfn1  13612  acsfn2  13614  iscat  13623  cidfval  13627  iscatd2  13632  monfval  13684  isfunc  13787  isfull2  13834  isfth2  13838  1stfval  14014  2ndfval  14017  yonedainv  14104  drsdirfi  14121  pospo  14156  mod1ile  14260  mod2ile  14261  isipodrs  14313  isacs4lem  14320  mrelatlub  14338  spwpr4  14389  submnd0  14451  resmhm  14485  mhmco  14488  mhmima  14489  pwsdiagmhm  14494  gsumwsubmcl  14510  gsumwmhm  14516  gsumwspan  14517  grprcan  14564  grplactcnv  14613  mulgz  14637  mulgnn0dir  14639  mulgdir  14641  mulgneg2  14643  mulgnn0ass  14645  mhmmulg  14648  pwssub  14657  pwsmulg  14658  issubg4  14687  nmzsubg  14707  ssnmz  14708  ghmmhmb  14743  resghm  14748  ghmpreima  14753  ghmnsgpreima  14756  ghmf1o  14761  isga  14794  gaid  14802  gass  14804  gapm  14809  gaorber  14811  gastacl  14812  gastacos  14813  lactghmga  14833  cntzsubm  14860  cntzsubg  14861  cntzmhm  14863  dfod2  14926  submod  14929  gexdvds  14944  gexcl3  14947  pgpfi  14965  sylow2blem3  14982  lsmub1x  15006  lsmless12  15021  pj1id  15057  efglem  15074  efgcpbllemb  15113  mulgnn0di  15174  eqgabl  15180  gexex  15194  torsubg  15195  cygabl  15226  prmcyg  15229  ghmcyg  15231  cyggexb  15234  gsumval3  15240  subgdmdprd  15318  mgpress  15385  isrng  15394  rngpropd  15421  dvdsrtr  15483  isdrng2  15571  issubrg  15594  cntzsubr  15626  abvrec  15650  abvdiv  15651  islmodd  15682  lmodprop2d  15736  lssvsubcl  15750  lssvacl  15760  lssvscl  15761  islss3  15765  lss1d  15769  lsspropd  15823  islmhm  15833  lmhmco  15849  lmhmplusg  15850  lmhmf1o  15852  lmhmima  15853  lmhmpreima  15854  reslmhm  15858  lspextmo  15862  pwsdiaglmhm  15863  lmhmpropd  15875  islbs2  15956  lidlsubcl  16017  drngnidl  16030  2idlcpbl  16035  unitrrg  16083  fidomndrng  16097  issubassa  16113  assapropd  16116  psrbaglefi  16167  psrbagconf1o  16169  coe1mul2lem1  16393  ply1coe  16417  qsssubdrg  16487  cnsubrg  16488  zlpir  16500  domnchr  16542  znval  16545  znunit  16573  znrrg  16575  isphl  16588  ocvlss  16628  ocvin  16630  obslbs  16686  toponmre  16886  neissex  16920  clslp  16935  tgrest  16946  restcld  16959  ssrest  16963  restopn2  16964  pnfnei  17006  mnfnei  17007  cnpnei  17049  cnco  17051  cnss1  17061  cnss2  17062  cncnp  17065  isnrm2  17142  restcnrm  17146  dnsconst  17162  cmpsub  17183  uncmp  17186  dfcon2  17201  2ndcrest  17236  1stcelcls  17243  subislly  17263  hausllycmp  17276  cldllycmp  17277  dislly  17279  kgencn  17307  ptpjpre2  17331  ptclsg  17365  dfac14  17368  ptcnplem  17371  txindis  17384  txlly  17386  txnlly  17387  pthaus  17388  txcmp  17393  xkohaus  17403  xkoptsub  17404  xkopt  17405  xkoinjcn  17437  qtopkgen  17457  kqdisj  17479  kqcldsat  17480  isr0  17484  kqreglem2  17489  kqnrmlem2  17491  nrmr0reg  17496  reghmph  17540  nrmhmph  17541  infil  17610  fgabs  17626  filcon  17630  trfil2  17634  isufil2  17655  trufil  17657  filssufilg  17658  ssufl  17665  ufileu  17666  rnelfm  17700  fbflim  17723  flimclsi  17725  flimsncls  17733  hauspwpwf1  17734  fclsval  17755  fclscf  17772  flimfnfcls  17775  uffclsflim  17778  alexsubb  17792  tmdmulg  17827  symgtgp  17836  xmetres2  17977  blhalf  18012  blssex  18025  blin2  18027  blbas  18028  met1stc  18119  met2ndci  18120  metcnpi  18142  metcnpi2  18143  dscopn  18148  ngpinvds  18186  subgngp  18203  tngngp  18222  nmdvr  18233  nlmvscn  18250  nrginvrcn  18254  lssnlm  18263  nmoco  18298  blcvx  18356  tgqioo  18358  icccmplem2  18380  xrge0tsms  18391  metdstri  18407  metdsle  18408  metdsre  18409  cncfss  18455  icoopnst  18490  phtpycc  18542  phtpc01  18547  pcohtpylem  18570  clmmulg  18644  nmoleub2lem2  18650  iscph  18659  ipcn  18726  csscld  18729  clsocv  18730  cfilfcls  18753  cmetcau  18768  iscmet3lem2  18771  lmclim  18781  flimcfil  18792  cmetss  18793  bcth  18804  bcth2  18805  ivthicc  18871  ovolficc  18881  ovolctb  18902  ovolun  18911  ovolfiniun  18913  ovoliunlem2  18915  ovoliunlem3  18916  ovolicc2lem3  18931  ovolicc2lem4  18932  unmbl  18948  shftmbl  18949  volfiniun  18957  voliunlem3  18962  volsup  18966  ioombl  18975  volcn  19014  volivth  19015  vitalilem1  19016  mbfconstlem  19037  mbfposr  19060  cnmbf  19067  mbflimsup  19074  i1fd  19089  i1f1  19098  itg10a  19118  itg2le  19147  itg2const2  19149  iblss  19212  itgeqa  19221  bddmulibl  19246  cnplimc  19290  limccnp2  19295  dvres  19314  dvnres  19333  dvcj  19352  dvrec  19357  dvmptfsum  19375  dvexp3  19378  dveflem  19379  dvlip2  19395  dvfsumrlimge0  19430  evlsval  19456  tdeglem4  19499  ply1domn  19562  elply2  19631  ply1termlem  19638  plypf1  19647  plymullem1  19649  dgrlem  19664  coeid  19673  coeeq2  19677  coemulc  19689  dgreq0  19699  dvply2g  19718  plydivalg  19732  plyexmo  19746  elqaa  19755  aaliou3lem8  19778  dvtaylp  19802  ulm2  19817  mtest  19834  abelthlem2  19861  ptolemy  19917  cosord  19947  logdivle  20026  divlogrlim  20035  logcnlem5  20046  efopn  20058  logtayl  20060  cxpmul2  20089  abscxp2  20093  cxplt  20094  cxple  20095  cxplt3  20100  atantayl3  20288  birthdaylem3  20301  rlimcnp2  20314  efrlim  20317  cxploglim2  20326  scvxcvx  20333  fta  20370  efnnfsumcl  20393  isppw2  20406  sqf11  20430  sgmval  20433  sgmval2  20434  efchtdvds  20450  sqff1o  20473  sgmmul  20493  pclogsum  20507  vmasum  20508  logfac2  20509  logexprlim  20517  perfect  20523  dchrelbas4  20535  dchrptlem2  20557  bcmax  20570  bposlem1  20576  bpos  20585  lgslem4  20591  lgsdir2lem5  20619  2sqlem6  20661  dchrisumlem3  20693  dchrmusum2  20696  pntrlog2bnd  20786  pntibnd  20795  pntlem3  20811  pnt3  20814  qabvexp  20828  ostth  20841  grpoidinvlem4  20927  grpoideu  20929  grpoidinv2  20938  rngo2  21108  blocnilem  21437  ipblnfi  21489  minvecolem4  21514  hvmul0or  21659  his35  21722  pjhtheu2  22050  3oalem2  22297  bralnfn  22583  kbpj  22591  eighmorth  22599  hmopm  22656  hmopco  22658  lnconi  22668  riesz3i  22697  cnlnadjlem6  22707  adjmul  22727  leopmuli  22768  nmopleid  22774  dmdbr2  22938  mdslmd1lem1  22960  superpos  22989  chirredlem2  23026  chirredi  23029  atcvat4i  23032  ifeqeqx  23144  iuninc  23154  disjdifprg  23160  xreceu  23320  xaddeq0  23339  xrsinvgval  23341  xrsmulgzz  23342  gsumpropd2lem  23357  xrge0tsmsd  23360  xpinpreima2  23374  sqsscirc2  23376  xrge0iifiso  23390  rge0scvg  23404  utoptop  23446  metustto  23495  metustexhalf  23498  metust  23500  cmetcusp  23512  elzrhunit  23558  qqhval2lem  23560  qqhf  23565  qqhghm  23567  gsumesum  23627  esumlub  23628  esumpr2  23634  esumfzf  23635  esumfsup  23636  esumpcvgval  23644  esumcvg  23652  sigainb  23695  insiga  23696  measiuns  23745  meascnbl  23747  measinb  23749  measdivcstOLD  23752  measdivcst  23753  dya2iocnrect  23805  dya2iocnei  23806  dya2iocucvr  23808  ballotlemfc0  23924  ballotlemfcc  23925  ballotlemsima  23947  subfacp1lem6  24000  pconcon  24046  conpcon  24050  sconpi1  24054  txscon  24056  cnllyscon  24060  cvmopnlem  24093  cvmfolem  24094  cvmlift  24114  umgra1  24162  sinccvg  24290  relexp0  24309  relexpindlem  24320  divelunit  24366  mulge0b  24372  ntrivcvgmullem  24406  prodmolem2  24438  prodmo  24439  zprod  24440  sltval2  24695  nodense  24728  nofulllem4  24744  colinearalglem4  24923  axcontlem2  24979  axcontlem4  24981  axcontlem7  24984  axcontlem8  24985  axcontlem9  24986  axcontlem10  24987  btwncomim  25022  btwnswapid  25026  lineext  25085  btwnconn1lem11  25106  btwnconn1lem14  25109  broutsideof3  25135  outsideoftr  25138  outsidele  25141  ellines  25161  linethru  25162  lxflflp1  25314  itg2addnclem  25317  itg2addnclem2  25318  locfindis  25454  neibastop2lem  25458  neibastop2  25459  sdclem1  25602  geomcau  25624  isbnd3  25656  prdstotbnd  25666  prdsbnd2  25667  ismtyhmeo  25677  heibor1  25682  rrnmet  25701  rrndstprj1  25702  rrncmslem  25704  rrncms  25705  iccbnd  25712  prter3  25898  elrfirn2  25919  mrefg3  25931  isnacs3  25933  mzprename  25975  eldioph2  25989  rexrabdioph  26023  rencldnfilem  26051  icodiamlt  26053  pellexlem3  26064  pellex  26068  pell14qrdich  26102  pellqrex  26112  pellfundex  26119  pellfund14b  26132  monotoddzzfi  26175  rpexpmord  26181  jm2.24  26198  congsym  26203  acongtr  26213  dvdsacongtr  26219  bezoutr  26220  bezoutr1  26221  jm2.18  26229  harinf  26275  kelac1  26309  lnmlsslnm  26327  dsmmbas2  26351  dsmmfi  26352  frlmlbs  26397  isnumbasgrplem3  26418  lindfind  26434  lindfrn  26439  islindf3  26444  hbt  26482  dgraalem  26498  mpaaeu  26503  f1omvdconj  26537  pmtrfinv  26550  symggen  26559  psgnunilem3  26567  grpvrinv  26599  matrng  26628  matassa  26629  mat1  26630  mendlmod  26649  acsfn1p  26655  proot1mul  26663  ofmul12  26690  ofdivdiv2  26693  fnchoice  26848  refsumcn  26849  fmuldfeq  26861  fmul01lt1lem1  26862  climsuselem1  26881  climsuse  26882  stoweidlem7  26904  stoweidlem14  26911  stoweidlem19  26916  stoweidlem20  26917  stoweidlem26  26923  stoweidlem27  26924  stoweidlem30  26927  stoweidlem31  26928  stoweidlem34  26931  stoweidlem35  26932  stoweidlem38  26935  stoweidlem39  26936  stoweidlem43  26940  stoweidlem44  26941  stoweidlem46  26943  stoweidlem48  26945  stoweidlem49  26946  stoweidlem52  26949  stoweidlem53  26950  stoweidlem54  26951  stoweidlem55  26952  stoweidlem56  26953  stoweidlem57  26954  stoweidlem58  26955  stoweidlem59  26956  stoweidlem60  26957  stoweidlem61  26958  stoweidlem62  26959  stoweid  26960  stirlinglem5  26975  afvco2  27189  ndmaovdistr  27220  prneimg  27228  uslgra1  27344  usgra1  27345  usgraedg4  27357  wlkres  27441  wlkbprop  27446  0pthon  27481  crcts  27505  cycls  27506  eupatrl  27523  constr3trllem5  27538  constr3cycllem1  27542  constr3cyclp  27546  3v3e3cycl  27549  4cycl4v4e  27550  4cycl4dv4e  27552  2pthfrgra  27603  frgrancvvdeqlemC  27631  onfrALTlem2  27805  2pm13.193  27812  onfrALTlem2VD  28176  lssats  29020  lfl0f  29077  ncvr1  29280  cvrletrN  29281  cvrnrefN  29290  iscvlat2N  29332  ltltncvr  29430  atcvrj2b  29439  atltcvr  29442  cvrat4  29450  islln3  29517  llnle  29525  2at0mat0  29532  islpln3  29540  islpln5  29542  islpln2a  29555  islvol3  29583  pmapglb2N  29778  pmapglb2xN  29779  isline3  29783  isline4N  29784  pmod1i  29855  pclbtwnN  29904  pclfinN  29907  pexmidN  29976  pexmidlem8N  29984  lhplt  30007  lhpexle1  30015  lhpjat1  30027  lhpj1  30029  lhpmcvr  30030  lhpmcvr2  30031  lhpm0atN  30036  lautcvr  30099  ldil1o  30119  ldilcnv  30122  ltrn1o  30131  ltrnid  30142  idltrn  30157  cdlemc3  30200  cdlemc4  30201  cdlemd1  30205  cdleme0cp  30221  cdleme0cq  30222  cdlemeulpq  30227  cdleme1  30234  cdleme2  30235  cdleme3b  30236  cdleme3c  30237  cdlemedb  30304  cdleme27a  30374  cdlemefrs32fva  30407  cdleme42keg  30493  cdleme42mgN  30495  cdleme48gfv  30544  cdlemf2  30569  cdlemg1a  30577  cdlemg1cex  30595  cdlemg5  30612  cdlemg4c  30619  trlcoat  30730  tgrpgrplem  30756  tendodi1  30791  tendodi2  30792  tendo0pl  30798  tendoicl  30803  tendoipl  30804  tendo0mul  30833  tendo0mulr  30834  dva1dim  30992  erngdvlem4  30998  erngdvlem4-rN  31006  tendospdi1  31028  dialss  31054  diaglbN  31063  diameetN  31064  dibglbN  31174  dib1dim2  31176  diblss  31178  dicssdvh  31194  diclss  31201  diclspsn  31202  dihlsscpre  31242  dihglblem5aN  31300  dihglblem4  31305  dihglblem5  31306  dih1dimatlem  31337  dihlsprn  31339  dihatlat  31342  dihglblem6  31348  dochvalr  31365
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
  Copyright terms: Public domain W3C validator