Theorem simpl 109

Description: Elimination of a conjunct. Theorem *3.26 (Simp) of [WhiteheadRussell] p. 112. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 13-Nov-2012.)

Assertion

Ref	Expression
simpl	|- ( ( ph /\ ps ) -> ph )

Proof of Theorem simpl

Step	Hyp	Ref	Expression
1		ax-ia1 106	1 |- ( ( ph /\ ps ) -> ph )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-ia1 106

This theorem is referenced by:  simpli  111  simpld  112  imp  124  adantrd  279  iba  300  pm3.41  331  pm4.45im  334  anim12  344  pm4.71  389  adantlr  477  adantrr  479  adantllr  481  adantlrr  483  adantrlr  485  adantrrr  487  simplll  535  simplrl  537  simprll  539  simprrl  541  anabs1  574  jcab  607  pm4.38  609  pm5.21  702  ioran  759  pm3.14  760  pm4.44  786  ordi  823  pm4.39  829  animorl  830  animorlr  832  pm5.16  835  pm5.54dc  925  intnanr  937  intnanrd  939  dcan  941  dedlema  977  dedlemb  978  pm4.42r  979  prlem2  982  ifpdc  987  dfifp2dc  989  simp1l  1047  simp2l  1049  simp3l  1051  3anandis  1383  xordc1  1437  anxordi  1444  falantru  1447  19.26  1529  exsimpl  1665  sbequ2  1817  sbcof2  1858  sbequilem  1886  sbequ8  1895  euan  2136  mooran1  2152  eupickbi  2162  2exeu  2172  dimatis  2197  rexim  2626  r19.26  2659  r19.40  2687  rspcime  2917  rr19.28v  2946  elrab3t  2961  eueq3dc  2980  mosubt  2983  reu6  2995  sbc2iegf  3102  sbcralt  3108  sbcrext  3109  rmob  3125  csbiebt  3167  ssab2  3311  difdif  3332  uneqin  3458  indifdir  3463  undif3ss  3468  rexm  3594  eqifdc  3642  ifandc  3646  ifnebibdc  3651  difsn  3810  opprc1  3884  unissel  3922  ssmin  3947  abssexg  4272  undifexmid  4283  pwntru  4289  exmidundif  4296  exmidundifim  4297  opelopabsb  4354  elopabran  4378  sess1  4434  ordelord  4478  onin  4483  suctr  4518  abnexg  4543  ifexg  4582  ordtriexmidlem  4617  ordtri2or2exmid  4669  ontri2orexmidim  4670  tfi  4680  peano1  4692  peano2  4693  nnpredcl  4721  0nelxp  4753  0nelelxp  4754  brab2a  4779  mosubopt  4791  posng  4798  opabssxp  4800  ideqg  4881  relssres  5051  trin2  5128  dminss  5151  iota4an  5307  iota2  5316  iotam  5318  fununfun  5373  fun11uni  5400  imadiflem  5409  funimaexg  5414  fneq12  5423  fvelrnb  5693  dffo4  5795  ffnfv  5805  ffvresb  5810  fmptco  5813  fcoconst  5818  funopsn  5830  fcof1  5924  isotr  5957  isopolem  5963  f1oiso  5967  acexmidlemcase  6013  ovprc1  6055  fnoprabg  6122  elovmporab  6222  elovmporab1w  6223  uchoice  6300  op1steq  6342  dmmpog  6374  1stconst  6386  f1o2ndf1  6393  brtpos2  6417  tpostpos  6430  tposf12  6435  smores  6458  tfrlemi1  6498  tfr1onlembfn  6510  tfri1dALT  6517  tfrcllembfn  6523  freceq1  6558  freceq2  6559  frectfr  6566  omv2  6633  omsuc  6640  nnsucelsuc  6659  nntri3  6665  nnaordi  6676  nnmordi  6684  nnm00  6698  ecexr  6707  ertr  6717  swoer  6730  erth  6748  ecelqsdm  6774  iinerm  6776  ecinxp  6779  erovlem  6796  pmresg  6845  resixp  6902  elixpsn  6904  mapsnf1o  6906  dom3  6949  modom  6994  mapdom1g  7033  ssenen  7037  phpelm  7053  finexdc  7092  exmidpweq  7101  nnwetri  7108  fiintim  7123  infidc  7133  ssfii  7173  fiss  7176  dcfi  7180  supubti  7198  supisoex  7208  ordiso2  7234  inl11  7264  omp1eomlem  7293  nnnninf  7325  nninfisol  7332  ctssexmid  7349  ismkvnex  7354  omniwomnimkv  7366  nninfwlpor  7373  nninfwlpoim  7378  nninfinfwlpo  7379  en2eleq  7406  en2other2  7407  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  acnrcl  7416  exmidaclem  7423  djuen  7426  djudoml  7434  netap  7473  2omotaplemst  7477  exmidapne  7479  cc1  7484  acnccim  7491  dmaddpqlem  7597  distrnqg  7607  ltanqi  7622  ltmnqi  7623  ltaddnq  7627  ltrnqg  7640  ltnnnq  7643  enq0sym  7652  addnq0mo  7667  mulnq0mo  7668  addnnnq0  7669  distrnq0  7679  prarloclemn  7719  prarloc  7723  ltdfpr  7726  genplt2i  7730  addnqprl  7749  addnqpru  7750  nqprl  7771  appdivnq  7783  1idprl  7810  1idpru  7811  ltexpri  7833  recexpr  7858  cauappcvgprlemdisj  7871  archrecpr  7884  addsrmo  7963  mulsrmo  7964  addsrpr  7965  mulsrpr  7966  0idsr  7987  1idsr  7988  archsr  8002  prsradd  8006  prsrlt  8007  caucvgsr  8022  map2psrprg  8025  elrealeu  8049  muladd11r  8335  negeu  8370  pncan  8385  pncan3  8387  negsub  8427  addid0  8552  posdif  8635  ltnegcon1  8643  subge0  8655  suble0  8656  lesub0  8659  reapval  8756  reapneg  8777  ap0gt0  8820  aprcl  8826  lt0ap0  8828  recextlem1  8831  recapb  8851  div0ap  8882  recrecap  8889  rec11ap  8890  recgt0  9030  mulgt1  9043  lerec2  9069  recp1lt1  9079  recreclt  9080  ledivp1  9083  negiso  9135  nnsub  9182  avglt1  9383  nnrecl  9400  nnnn0addcl  9432  elnn0nn  9444  nn0ge2m1nn  9462  zaddcl  9519  eluzmn  9762  eluzadd  9785  infregelbex  9832  divfnzn  9855  qaddcl  9869  qreccl  9876  cnref1o  9885  ge0p1rp  9920  divlt1lt  9959  divle1le  9960  addlelt  10003  xrre3  10057  xltnegi  10070  xaddval  10080  xaddcom  10096  xnegdi  10103  xposdif  10117  ixxssixx  10137  iccshftr  10229  iccshftl  10231  iccdil  10233  icccntr  10235  zltaddlt1le  10242  elfz2  10250  peano2fzr  10272  fzdcel  10275  fzsplit2  10285  fzaddel  10294  fzrev2  10320  fzrev2i  10321  fzrev3  10322  elfz1b  10325  fseq1p1m1  10329  uzsubfz0  10364  fzosubel3  10442  eluzgtdifelfzo  10443  fzofzp1b  10474  elfzomelpfzo  10477  exfzdc  10487  fvinim0ffz  10488  zsupcllemex  10491  infssuzcldc  10496  exbtwnzlemshrink  10509  qbtwnz  10512  qbtwnxr  10518  ico0  10522  elicore  10527  xqltnle  10528  apbtwnz  10535  flqge  10543  flqlt  10544  flqltnz  10548  flqbi2  10552  flqaddz  10558  flqmulnn0  10560  intfracq  10583  flqdiv  10584  q0mod  10618  q1mod  10619  mulp1mod1  10628  q2txmodxeq0  10647  modfzo0difsn  10658  frec2uzuzd  10665  frec2uzltd  10666  frec2uzrand  10668  uzennn  10699  seqfveq2g  10740  seq3split  10751  seqsplitg  10752  seq3caopr  10758  seqcaoprg  10759  seqf1oglem2  10783  seqf1og  10784  exp3vallem  10803  exp3val  10804  expnnval  10805  exp1  10808  expcl2lemap  10814  rpexpcl  10821  expnegzap  10836  mulexp  10841  mulexpzap  10842  leexp2r  10856  leexp1a  10857  sq11  10875  subsq  10909  binom2  10914  binom3  10920  zesq  10921  bernneq  10923  sq11ap  10970  zzlesq  10971  mulsubdivbinom2ap  10974  apexp1  10981  facwordi  11003  facubnd  11008  facavg  11009  bcval  11012  bcval5  11026  hashennn  11043  fihashf1rn  11051  fseq1hash  11065  hashdifsn  11084  hashdifpr  11085  hashxp  11091  fiubz  11094  fiubnn  11095  fnfz0hash  11097  ffzo0hash  11099  hash2en  11108  wrdval  11120  ffz0iswrdnn0  11144  wrdsymb0  11150  ccatsymb  11183  ccatval21sw  11186  lswccatn0lsw  11192  ccatalpha  11194  ccatrcl1  11195  s111  11212  ccat1st1st  11222  lswccats1fst  11225  swrdlen2  11247  swrdfv2  11248  swrdsbslen  11251  swrds1  11253  ccatswrd  11255  pfxval  11259  pfxclg  11263  pfxmpt  11265  pfxid  11271  pfxfv0  11277  pfxtrcfv0  11279  pfxfvlsw  11280  pfxeq  11281  ccatpfx  11286  swrdpfx  11292  lenrevpfxcctswrd  11297  wrdeqs1cat  11305  cats1un  11306  swrdccatin1  11310  pfxccatin12lem2a  11312  pfxccatin12lem1  11313  pfxccatin12lem3  11317  pfxccatin12  11318  swrdccat  11320  pfxccat3a  11323  swrdccat3blem  11324  swrdccat3b  11325  reuccatpfxs1lem  11331  reuccatpfxs1  11332  s2cl  11370  s2fv0g  11372  shftfvalg  11396  ovshftex  11397  shftdm  11400  shftfib  11401  shftval  11403  shftf  11408  crre  11435  cjexp  11471  cjreim2  11482  uzin2  11565  rexuz3  11568  resqrexlemgt0  11598  resqrex  11604  sqrtgt0  11612  sqrtsq  11622  sqrtmsq  11623  absrpclap  11639  absext  11641  absmul  11647  absid  11649  absexp  11657  nn0abscl  11663  abslt  11666  absle  11667  recvalap  11675  abstri  11682  caubnd2  11695  qdenre  11780  maxabsle  11782  maxabslemval  11786  maxcl  11788  rexanre  11798  min1inf  11810  minabs  11814  minclpr  11815  mul0inf  11819  mingeb  11820  xrmaxiflemcl  11823  xrnegiso  11840  climconst2  11869  climmpt  11878  climres  11881  climcaucn  11929  sumeq1  11933  summodclem2a  11960  isumz  11968  fisumss  11971  fsumzcl2  11984  sumsnf  11988  isumclim3  12002  fsum2dlemstep  12013  fisumcom2  12017  fsumconst  12033  cvgcmpub  12055  binom  12063  binom1p  12064  binom1dif  12066  bcxmas  12068  divcnv  12076  geo2lim  12095  geoisum  12096  geoisumr  12097  geoisum1  12098  mertenslemi1  12114  mertensabs  12116  prod1dc  12165  fprodconst  12199  fprodcom2fi  12205  efcllem  12238  efcj  12252  efadd  12254  efexp  12261  efgt1p2  12274  tanvalap  12287  tanval2ap  12292  tanval3ap  12293  sinadd  12315  cosadd  12316  dvdsdc  12377  iddvdsexp  12394  dvdsadd  12415  dvds1  12432  odd2np1  12452  oddm1even  12454  m1exp1  12480  divalglemnn  12497  fldivndvdslt  12516  flodddiv4lt  12517  bitsp1  12530  bitsmod  12535  bitsfi  12536  bitscmp  12537  bitsinv1lem  12540  dvdsbnd  12545  gcdnncl  12556  zeqzmulgcd  12559  gcdneg  12571  modgcd  12580  bezoutlemex  12590  bezoutlemeu  12596  dfgcd3  12599  gcdzeq  12611  dvdssq  12620  algrf  12635  eucalgval2  12643  eucalgcvga  12648  lcmval  12653  gcddvdslcm  12663  lcmneg  12664  coprmgcdb  12678  qredeu  12687  divgcdcoprm0  12691  divgcdcoprmex  12692  cncongr1  12693  cncongr2  12694  cncongrcoprm  12696  prmind2  12710  dvdsnprmd  12715  exprmfct  12728  isprm6  12737  pw2dvdslemn  12755  oddpwdclemdc  12763  sqrt2irraplemnn  12769  divnumden  12786  divdenle  12787  nn0sqrtelqelz  12796  phivalfi  12802  crth  12814  eulerth  12823  prmdivdiv  12827  reumodprminv  12844  nnnn0modprm0  12846  nnoddn2prmb  12853  pcval  12887  pcidlem  12914  pcid  12915  pcneg  12916  pc2dvds  12921  pcz  12923  pcprod  12937  prmpwdvds  12946  4sqexercise1  12989  2expltfac  13030  xpct  13035  znnen  13037  ennnfonelemg  13042  ennnfone  13064  ctinfom  13067  ctinf  13069  ssomct  13084  isstruct2im  13110  isstruct2r  13111  setsvalg  13130  setsslnid  13152  ressvalsets  13165  ressex  13166  2strbasg  13221  2stropg  13222  2strbas1g  13224  ressmulrg  13246  ressscag  13284  ressvscag  13285  ressipg  13286  restval  13346  restid2  13349  prdsex  13370  pwsval  13392  qusex  13426  fnpr2o  13440  xpsfval  13449  xpsval  13453  intopsn  13468  mgmidmo  13473  lidrididd  13483  ismnddef  13519  mndinvmod  13546  imasmnd2  13553  ismhm  13562  mhmex  13563  insubm  13586  dfgrp2  13628  grpsubval  13647  grpinvinv  13668  grpsubrcan  13682  grpsubadd  13689  grpaddsubass  13691  grpsubsub4  13694  grppnpcan2  13695  grpnpncan  13696  grpnpncan0  13697  grpnnncan2  13698  dfgrp3m  13700  dfgrp3me  13701  imasgrp2  13715  mhmmnd  13721  mulgfvalg  13726  mulgval  13727  mulgfng  13729  mulg1  13734  mulgnnp1  13735  mulgnndir  13756  mulgass  13764  mulgmodid  13766  issubg2m  13794  grpissubg  13799  isnsg  13807  isnsg3  13812  0nsg  13819  eqgfval  13827  eqger  13829  eqgen  13832  eqgcpbl  13833  quseccl  13838  isghm  13848  kerf1ghm  13879  conjghm  13881  conjsubg  13882  abladdsub  13920  ablpncan3  13922  ablsubsub23  13930  invghm  13934  subgabl  13937  mgpress  13963  rngdi  13972  rnglz  13977  imasrng  13988  srgmulgass  14021  srgrmhm  14026  isring  14032  ringo2times  14060  ringrng  14068  ringlz  14075  imasring  14096  opprrng  14109  opprrngbg  14110  opprring  14111  mulgass3  14117  dvdsrd  14127  dvdsrneg  14136  unitnegcl  14163  dvrvald  14167  dvrid  14170  dvr1  14171  dvrass  14172  dvrdir  14176  ringinvdv  14178  rhmex  14190  isrim0  14194  rhmval  14206  rhmdvdsr  14208  rhmopp  14209  elrhmunit  14210  rhmunitinv  14211  isnzr2  14217  ringelnzr  14220  issubrng2  14243  issubrg2  14274  aprap  14319  lmodvs1  14349  lmod0vs  14354  lmodvs0  14355  lmodvsmmulgdi  14356  lmodfopne  14359  lmodvneg1  14363  lss1  14395  islss3  14412  lsslss  14414  lss1d  14416  lspf  14422  lspsn  14449  lspsnneg  14453  sraval  14470  sraring  14482  qus1  14559  qusrhm  14561  cnfldui  14622  dvdsrzring  14636  mulgghm2  14641  mulgrhm  14642  znval  14669  znf1o  14684  psrbagfi  14706  psrplusgg  14711  mplgrpfi  14739  eltg2b  14797  difopn  14851  ntrcls0  14874  neii1  14890  restbasg  14911  resttopon  14914  restuni2  14920  cnrest2r  14980  tx1cn  15012  txcnp  15014  txcn  15018  txswaphmeo  15064  psmettri  15073  xmeteq0  15102  xmettri  15115  metrtri  15120  ssblex  15174  xmeter  15179  isxms2  15195  cnbl0  15277  cnblcld  15278  reopnap  15289  tgioo  15297  addcncntoplem  15304  expcn  15312  rescncf  15324  cncfcdm  15325  mulc1cncf  15332  cncfcncntop  15336  addccncf  15343  cdivcncfap  15347  negcncf  15348  cnopnap  15354  suplociccex  15368  hoverlt1  15392  hovergt0  15393  dich0  15395  limccl  15402  ellimc3apf  15403  cnplimcim  15410  limccnp2lem  15419  reldvg  15422  dvbsssg  15429  dvcjbr  15451  dvcj  15452  dvfre  15453  dvrecap  15456  dvef  15470  plyaddcl  15497  plymulcl  15498  plysubcl  15499  plyrecj  15506  reeff1olem  15514  pilem3  15526  ptolemy  15567  rplogcl  15622  rpcxpef  15637  cxprec  15653  rpcxproot  15657  rplogb1  15691  logbgt0b  15709  logbgcd1irr  15710  binom4  15722  wilthlem1  15723  sgmnncl  15731  dvdsppwf1o  15732  mersenne  15740  lgslem4  15751  lgsval  15752  lgsval2lem  15758  lgsval4a  15770  lgsdir2lem3  15778  lgsdir2  15781  lgsne0  15786  lgsprme0  15790  lgsmulsqcoprm  15794  gausslemma2dlem0a  15797  gausslemma2dlem1a  15806  2lgslem1b  15837  2lgslem2  15840  2lgsoddprm  15861  struct2slots2dom  15908  structvtxval  15909  structiedg0val  15910  struct2griedg  15916  edgstruct  15934  uhgr0vb  15954  incistruhgr  15960  umgrvad2edg  16081  uspgredg2vlem  16090  uspgredg2v  16091  usgredg2v  16094  ushgredgedg  16096  ushgredgedgloop  16098  usgr0vb  16103  uhgr0vusgr  16108  edg0usgr  16117  subupgr  16143  upgrspanop  16153  umgrspanop  16154  usgrspanop  16155  vtxdgfval  16158  wksfval  16192  wlkpropg  16194  uspgr2wlkeq2  16236  uspgr2wlkeqi  16237  upgr2wlkdc  16247  trlsex  16257  clwwlkccatlem  16270  clwwlkng  16275  clwwlkext2edg  16292  clwwlknccat  16293  umgr2cwwkdifex  16295  clwwlknonel  16302  clwwlknonccat  16303  clwwlknonex2lem2  16308  clwwlknun  16311  eupthsg  16315  eupth2lem3lem6fi  16341  bj-nnan  16383  bj-indind  16578  bj-omtrans  16602  bj-inf2vnlem1  16616  sscoll2  16634  2omap  16645  pw1map  16647  pwtrufal  16649  sssneq  16654  pw1nct  16655  nninfsellemsuc  16665  nninfomnilem  16671  nnnninfex  16675  exmidsbthrlem  16677  qdencn  16682  trilpo  16698  trirec0  16699  apdiff  16703  iswomninnlem  16705  iswomni0  16707  redcwlpo  16711  redc0  16713  reap0  16714  cndcap  16715  dceqnconst  16716  dcapnconst  16717  neapmkv  16724  neap0mkv  16725