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  2526  rmob  3079  ifboth  3596  ordelord  4414  poinxp  4753  soltmin  5082  sofld  5121  f1oprswap  5515  mpteqb  5614  fvmptt  5615  iinpreima  5655  fcof1  5797  soisoi  5825  grprinvlem  6058  fnfvof  6090  dftpos4  6253  tfrlem9a  6402  oaass  6559  oelimcl  6598  nnawordex  6635  oaabs  6642  oaabs2  6643  omabs  6645  qsel  6738  th3qlem1  6764  mapss  6810  boxcutc  6859  omxpenlem  6963  xpmapenlem  7028  mapdom2  7032  unxpdomlem3  7069  f1finf1o  7086  frfi  7102  nnunifi  7108  indexfi  7163  elfi2  7168  elfiun  7183  marypha1lem  7186  supisolem  7221  ordtypelem7  7239  oismo  7255  wdomtr  7289  brwdom3  7296  cnfcomlem  7402  r1ordg  7450  rankval3b  7498  rankonidlem  7500  harcard  7611  infxpenlem  7641  acni2  7673  numacn  7676  acndom2  7681  fodomacn  7683  mappwen  7739  dfac9  7762  cdalepw  7822  infxpabs  7838  infunsdom1  7839  infunsdom  7840  ackbij1lem15  7860  cfsmolem  7896  infpssrlem5  7933  infpssr  7934  ssfin4  7936  fin2i2  7944  ssfin2  7946  fin23lem24  7948  fin23lem22  7953  fin23lem27  7954  fin23lem36  7974  isf32lem3  7981  isf32lem7  7985  isf34lem7  8005  fin1a2lem13  8038  hsmexlem4  8055  axdc4lem  8081  ttukeylem6  8141  iundom2g  8162  alephexp1  8201  fpwwe2lem1  8253  fpwwe2lem8  8259  fpwwe2lem12  8263  canthp1  8276  inttsk  8396  inar1  8397  r1tskina  8404  grur1  8442  nqerf  8554  distrlem1pr  8649  distrlem4pr  8650  reclem2pr  8672  addsub4  9090  le2add  9256  lt2sub  9272  le2sub  9273  mulge0  9291  receu  9413  rec11  9458  rec11r  9459  divdivdiv  9461  ddcan  9474  divadddiv  9475  divsubdiv  9476  conjmul  9477  rereccl  9478  subrec  9589  recgt0  9600  prodgt0  9601  prodge0  9603  ltmul12a  9612  lemul12a  9614  lemulge11  9618  lt2mul2div  9632  ltrec  9637  lerec  9638  lt2msq  9640  le2msq  9656  msq11  9657  ledivp1  9658  rimul  9737  zsupss  10307  uzwo3  10311  qreccl  10336  rpnnen1lem1  10342  rpnnen1lem2  10343  rpnnen1lem3  10344  rpnnen1lem5  10346  qbtwnre  10526  qbtwnxr  10527  xralrple  10532  xpncan  10571  xaddge0  10578  xle2add  10579  xmulneg1  10589  xmulgt0  10603  ixxss1  10674  ixxss2  10675  elioc2  10713  difreicc  10767  fzass4  10829  fzrev  10846  modid  10993  uzindi  11043  seqfeq3  11096  expcl2lem  11115  expnegz  11136  expadd  11144  expmul  11147  expcan  11154  ltexp2  11155  leexp1a  11160  expnlbnd  11231  digit1  11235  bcval5  11330  bcpasc  11333  fzsdom2  11382  hashbclem  11390  hashbc  11391  hashf1lem2  11394  seqcoll  11401  ccatswrd  11459  revccat  11484  sqrmul  11745  sqrlt  11747  sqrdiv  11751  absexpz  11790  abslt  11798  absle  11799  abssubne0  11800  rexico  11837  amgm2  11853  rlim3  11972  lo1bdd2  11998  climuni  12026  rlimcn1  12062  cn1lem  12071  iserex  12130  iserle  12133  isercolllem1  12138  climcau  12144  caucvgb  12152  iseralt  12157  summo  12190  zsum  12191  sumss2  12199  isumadd  12230  fsum2dlem  12233  fsum2d  12234  fsum0diag2  12245  fsumabs  12259  cvgcmp  12274  cvgcmpce  12276  incexclem  12295  incexc2  12297  isumsplit  12299  climcnds  12310  divrcnv  12311  geolim  12326  geo2lim  12331  geomulcvg  12332  mertenslem1  12340  mertenslem2  12341  mertens  12342  efcvgfsum  12367  eftlcl  12387  reeftlcl  12388  tanadd  12447  eirr  12483  rpnnen2  12504  sqr2irr  12527  dvds2ln  12559  dvdseq  12576  dvdsext  12579  bitsfzo  12626  sadadd2lem2  12641  sadadd  12658  bitsshft  12666  smupvallem  12674  smumul  12684  bezout  12721  gcdmultiplez  12730  dvdsmulgcd  12733  prmdvdsexp  12793  pcqmul  12906  pcexp  12912  pcneg  12926  pcdvdstr  12928  pcprmpw2  12934  pcfac  12947  expnprm  12950  prmpwdvds  12951  prmreclem6  12968  mul4sq  13001  vdwapf  13019  vdwlem13  13040  vdw  13041  vdwnnlem3  13044  vdwnn  13045  ramub2  13061  ramz  13072  ramcl  13076  ressress  13205  pwsle  13391  mreriincl  13500  mrcuni  13523  mreexexlemd  13546  isacs2  13555  acsfn  13561  acsfn1  13563  acsfn2  13565  iscat  13574  cidfval  13578  iscatd2  13583  monfval  13635  isfunc  13738  isfull2  13785  isfth2  13789  1stfval  13965  2ndfval  13968  yonedainv  14055  drsdirfi  14072  pospo  14107  mod1ile  14211  mod2ile  14212  isipodrs  14264  isacs4lem  14271  mrelatlub  14289  spwpr4  14340  submnd0  14402  resmhm  14436  mhmco  14439  mhmima  14440  pwsdiagmhm  14445  gsumwsubmcl  14461  gsumwmhm  14467  gsumwspan  14468  grprcan  14515  grplactcnv  14564  mulgz  14588  mulgnn0dir  14590  mulgdir  14592  mulgneg2  14594  mulgnn0ass  14596  mhmmulg  14599  pwssub  14608  pwsmulg  14609  issubg4  14638  nmzsubg  14658  ssnmz  14659  ghmmhmb  14694  resghm  14699  ghmpreima  14704  ghmnsgpreima  14707  ghmf1o  14712  isga  14745  gaid  14753  gass  14755  gapm  14760  gaorber  14762  gastacl  14763  gastacos  14764  lactghmga  14784  cntzsubm  14811  cntzsubg  14812  cntzmhm  14814  dfod2  14877  submod  14880  gexdvds  14895  gexcl3  14898  pgpfi  14916  sylow2blem3  14933  lsmub1x  14957  lsmless12  14972  pj1id  15008  efglem  15025  efgcpbllemb  15064  mulgnn0di  15125  eqgabl  15131  gexex  15145  torsubg  15146  cygabl  15177  prmcyg  15180  ghmcyg  15182  cyggexb  15185  gsumval3  15191  subgdmdprd  15269  mgpress  15336  isrng  15345  rngpropd  15372  dvdsrtr  15434  isdrng2  15522  issubrg  15545  cntzsubr  15577  abvrec  15601  abvdiv  15602  islmodd  15633  lmodprop2d  15687  lssvsubcl  15701  lssvacl  15711  lssvscl  15712  islss3  15716  lss1d  15720  lsspropd  15774  islmhm  15784  lmhmco  15800  lmhmplusg  15801  lmhmf1o  15803  lmhmima  15804  lmhmpreima  15805  reslmhm  15809  lspextmo  15813  pwsdiaglmhm  15814  lmhmpropd  15826  islbs2  15907  lidlsubcl  15968  drngnidl  15981  2idlcpbl  15986  unitrrg  16034  fidomndrng  16048  issubassa  16064  assapropd  16067  psrbaglefi  16118  psrbagconf1o  16120  coe1mul2lem1  16344  ply1coe  16368  qsssubdrg  16431  cnsubrg  16432  zlpir  16444  domnchr  16486  znval  16489  znunit  16517  znrrg  16519  isphl  16532  ocvlss  16572  ocvin  16574  obslbs  16630  toponmre  16830  neissex  16864  clslp  16879  tgrest  16890  restcld  16903  ssrest  16907  restopn2  16908  pnfnei  16950  mnfnei  16951  cnpnei  16993  cnco  16995  cnss1  17005  cnss2  17006  cncnp  17009  isnrm2  17086  restcnrm  17090  dnsconst  17106  cmpsub  17127  uncmp  17130  dfcon2  17145  2ndcrest  17180  1stcelcls  17187  subislly  17207  hausllycmp  17220  cldllycmp  17221  dislly  17223  kgencn  17251  ptpjpre2  17275  ptclsg  17309  dfac14  17312  ptcnplem  17315  txindis  17328  txlly  17330  txnlly  17331  pthaus  17332  txcmp  17337  xkohaus  17347  xkoptsub  17348  xkopt  17349  xkoinjcn  17381  qtopkgen  17401  kqdisj  17423  kqcldsat  17424  isr0  17428  kqreglem2  17433  kqnrmlem2  17435  nrmr0reg  17440  reghmph  17484  nrmhmph  17485  infil  17558  fgabs  17574  filcon  17578  trfil2  17582  isufil2  17603  trufil  17605  filssufilg  17606  ssufl  17613  ufileu  17614  rnelfm  17648  fbflim  17671  flimclsi  17673  flimsncls  17681  hauspwpwf1  17682  fclsval  17703  fclscf  17720  flimfnfcls  17723  uffclsflim  17726  alexsubb  17740  tmdmulg  17775  symgtgp  17784  xmetres2  17925  blhalf  17960  blssex  17973  blin2  17975  blbas  17976  met1stc  18067  met2ndci  18068  metcnpi  18090  metcnpi2  18091  dscopn  18096  ngpinvds  18134  subgngp  18151  tngngp  18170  nmdvr  18181  nlmvscn  18198  nrginvrcn  18202  lssnlm  18211  nmoco  18246  blcvx  18304  tgqioo  18306  icccmplem2  18328  xrge0tsms  18339  metdstri  18355  metdsle  18356  metdsre  18357  cncfss  18403  icoopnst  18437  phtpycc  18489  phtpc01  18494  pcohtpylem  18517  clmmulg  18591  nmoleub2lem2  18597  iscph  18606  ipcn  18673  csscld  18676  clsocv  18677  cfilfcls  18700  cmetcau  18715  iscmet3lem2  18718  lmclim  18728  flimcfil  18739  cmetss  18740  bcth  18751  bcth2  18752  ivthicc  18818  ovolficc  18828  ovolctb  18849  ovolun  18858  ovolfiniun  18860  ovoliunlem2  18862  ovoliunlem3  18863  ovolicc2lem3  18878  ovolicc2lem4  18879  unmbl  18895  shftmbl  18896  volfiniun  18904  voliunlem3  18909  volsup  18913  ioombl  18922  volcn  18961  volivth  18962  vitalilem1  18963  mbfconstlem  18984  mbfposr  19007  cnmbf  19014  mbflimsup  19021  i1fd  19036  i1f1  19045  itg10a  19065  itg2le  19094  itg2const2  19096  iblss  19159  itgeqa  19168  bddmulibl  19193  cnplimc  19237  limccnp2  19242  dvres  19261  dvnres  19280  dvcj  19299  dvrec  19304  dvmptfsum  19322  dvexp3  19325  dveflem  19326  dvlip2  19342  dvfsumrlimge0  19377  evlsval  19403  tdeglem4  19446  ply1domn  19509  elply2  19578  ply1termlem  19585  plypf1  19594  plymullem1  19596  dgrlem  19611  coeid  19620  coeeq2  19624  coemulc  19636  dgreq0  19646  dvply2g  19665  plydivalg  19679  plyexmo  19693  elqaa  19702  aaliou3lem8  19725  dvtaylp  19749  ulm2  19764  mtest  19781  abelthlem2  19808  ptolemy  19864  cosord  19894  logdivle  19973  divlogrlim  19982  logcnlem5  19993  efopn  20005  logtayl  20007  cxpmul2  20036  abscxp2  20040  cxplt  20041  cxple  20042  cxplt3  20047  atantayl3  20235  birthdaylem3  20248  rlimcnp2  20261  efrlim  20264  cxploglim2  20273  scvxcvx  20280  fta  20317  efnnfsumcl  20340  isppw2  20353  sqf11  20377  sgmval  20380  sgmval2  20381  efchtdvds  20397  sqff1o  20420  sgmmul  20440  pclogsum  20454  vmasum  20455  logfac2  20456  logexprlim  20464  perfect  20470  dchrelbas4  20482  dchrptlem2  20504  bcmax  20517  bposlem1  20523  bpos  20532  lgslem4  20538  lgsdir2lem5  20566  2sqlem6  20608  dchrisumlem3  20640  dchrmusum2  20643  pntrlog2bnd  20733  pntibnd  20742  pntlem3  20758  pnt3  20761  qabvexp  20775  ostth  20788  grpoidinvlem4  20874  grpoideu  20876  grpoidinv2  20885  rngo2  21055  blocnilem  21382  ipblnfi  21434  minvecolem4  21459  hvmul0or  21604  his35  21667  pjhtheu2  21995  3oalem2  22242  bralnfn  22528  kbpj  22536  eighmorth  22544  hmopm  22601  hmopco  22603  lnconi  22613  riesz3i  22642  cnlnadjlem6  22652  adjmul  22672  leopmuli  22713  nmopleid  22719  dmdbr2  22883  mdslmd1lem1  22905  superpos  22934  chirredlem2  22971  chirredi  22974  atcvat4i  22977  ifeqeqx  23034  ballotlemfc0  23051  ballotlemfcc  23052  ballotlemsima  23074  xreceu  23105  iuninc  23158  xpinpreima2  23291  sqsscirc2  23293  xaddeq0  23304  xrsinvgval  23306  xrsmulgzz  23307  xrge0iifiso  23317  disjdifprg  23352  rge0scvg  23373  gsumpropd2lem  23379  xrge0tsmsd  23382  esumpr2  23439  esumpcvgval  23446  esumcvg  23454  sigainb  23497  insiga  23498  measiuns  23544  meascnbl  23546  measinb  23548  measdivcstOLD  23551  measdivcst  23552  subfacp1lem6  23716  pconcon  23762  conpcon  23766  sconpi1  23770  txscon  23772  cnllyscon  23776  cvmopnlem  23809  cvmfolem  23810  cvmlift  23830  umgra1  23878  sinccvg  24006  relexp0  24025  relexpindlem  24036  divelunit  24080  mulge0b  24086  sltval2  24310  nodense  24343  nofulllem4  24359  colinearalglem4  24537  axcontlem2  24593  axcontlem4  24595  axcontlem7  24598  axcontlem8  24599  axcontlem9  24600  axcontlem10  24601  btwncomim  24636  btwnswapid  24640  lineext  24699  btwnconn1lem11  24720  btwnconn1lem14  24723  broutsideof3  24749  outsideoftr  24752  outsidele  24755  ellines  24775  linethru  24776  cbicp  25166  geme2  25275  ranncnt  25283  trran2  25393  ltrran2  25403  ltrinvlem  25406  osneisi  25531  qusp  25542  cnpflf4  25564  limptlimpr2lem1  25574  iintlem1  25610  flfneicn  25625  addcanrg  25667  subaddv  25671  distmlva  25688  icccon3  25701  icmpmon  25816  iepiclem  25823  locfindis  26305  neibastop2lem  26309  neibastop2  26310  sdclem1  26453  geomcau  26475  isbnd3  26508  prdstotbnd  26518  prdsbnd2  26519  ismtyhmeo  26529  heibor1  26534  rrnmet  26553  rrndstprj1  26554  rrncmslem  26556  rrncms  26557  iccbnd  26564  prter3  26750  elrfirn2  26771  mrefg3  26783  isnacs3  26785  mzprename  26827  eldioph2  26841  rexrabdioph  26875  rencldnfilem  26903  icodiamlt  26905  pellexlem3  26916  pellex  26920  pell14qrdich  26954  pellqrex  26964  pellfundex  26971  pellfund14b  26984  monotoddzzfi  27027  rpexpmord  27033  jm2.24  27050  congsym  27055  acongtr  27065  dvdsacongtr  27071  bezoutr  27072  bezoutr1  27073  jm2.18  27081  harinf  27127  kelac1  27161  lnmlsslnm  27179  dsmmbas2  27203  dsmmfi  27204  frlmlbs  27249  isnumbasgrplem3  27270  lindfind  27286  lindfrn  27291  islindf3  27296  hbt  27334  dgraalem  27350  mpaaeu  27355  f1omvdconj  27389  pmtrfinv  27402  symggen  27411  psgnunilem3  27419  grpvrinv  27451  matrng  27480  matassa  27481  mat1  27482  mendlmod  27501  acsfn1p  27507  proot1mul  27515  ofmul12  27542  ofdivdiv2  27545  fnchoice  27700  refsumcn  27701  fmuldfeq  27713  fmul01lt1lem1  27714  climsuselem1  27733  climsuse  27734  stoweidlem7  27756  stoweidlem14  27763  stoweidlem19  27768  stoweidlem20  27769  stoweidlem26  27775  stoweidlem27  27776  stoweidlem30  27779  stoweidlem31  27780  stoweidlem34  27783  stoweidlem35  27784  stoweidlem38  27787  stoweidlem39  27788  stoweidlem43  27792  stoweidlem44  27793  stoweidlem46  27795  stoweidlem48  27797  stoweidlem49  27798  stoweidlem52  27801  stoweidlem53  27802  stoweidlem54  27803  stoweidlem55  27804  stoweidlem56  27805  stoweidlem57  27806  stoweidlem58  27807  stoweidlem59  27808  stoweidlem60  27809  stoweidlem61  27810  stoweidlem62  27811  stoweid  27812  stirlinglem5  27827  afvco2  28037  ndmaovdistr  28067  prneimg  28073  uslgra1  28118  usgra1  28119  onfrALTlem2  28311  2pm13.193  28318  onfrALTlem2VD  28665  lssats  29202  lfl0f  29259  ncvr1  29462  cvrletrN  29463  cvrnrefN  29472  iscvlat2N  29514  ltltncvr  29612  atcvrj2b  29621  atltcvr  29624  cvrat4  29632  islln3  29699  llnle  29707  2at0mat0  29714  islpln3  29722  islpln5  29724  islpln2a  29737  islvol3  29765  pmapglb2N  29960  pmapglb2xN  29961  isline3  29965  isline4N  29966  pmod1i  30037  pclbtwnN  30086  pclfinN  30089  pexmidN  30158  pexmidlem8N  30166  lhplt  30189  lhpexle1  30197  lhpjat1  30209  lhpj1  30211  lhpmcvr  30212  lhpmcvr2  30213  lhpm0atN  30218  lautcvr  30281  ldil1o  30301  ldilcnv  30304  ltrn1o  30313  ltrnid  30324  idltrn  30339  cdlemc3  30382  cdlemc4  30383  cdlemd1  30387  cdleme0cp  30403  cdleme0cq  30404  cdlemeulpq  30409  cdleme1  30416  cdleme2  30417  cdleme3b  30418  cdleme3c  30419  cdlemedb  30486  cdleme27a  30556  cdlemefrs32fva  30589  cdleme42keg  30675  cdleme42mgN  30677  cdleme48gfv  30726  cdlemf2  30751  cdlemg1a  30759  cdlemg1cex  30777  cdlemg5  30794  cdlemg4c  30801  trlcoat  30912  tgrpgrplem  30938  tendodi1  30973  tendodi2  30974  tendo0pl  30980  tendoicl  30985  tendoipl  30986  tendo0mul  31015  tendo0mulr  31016  dva1dim  31174  erngdvlem4  31180  erngdvlem4-rN  31188  tendospdi1  31210  dialss  31236  diaglbN  31245  diameetN  31246  dibglbN  31356  dib1dim2  31358  diblss  31360  dicssdvh  31376  diclss  31383  diclspsn  31384  dihlsscpre  31424  dihglblem5aN  31482  dihglblem4  31487  dihglblem5  31488  dih1dimatlem  31519  dihlsprn  31521  dihatlat  31524  dihglblem6  31530  dochvalr  31547
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