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  703  ioran  760  pm3.14  761  pm4.44  787  ordi  824  pm4.39  830  animorl  831  animorlr  833  pm5.16  836  pm5.54dc  926  intnanr  938  intnanrd  940  dcan  942  dedlema  978  dedlemb  979  pm4.42r  980  prlem2  983  ifpdc  988  dfifp2dc  990  simp1l  1048  simp2l  1050  simp3l  1052  3anandis  1384  xordc1  1438  anxordi  1445  falantru  1448  19.26  1530  exsimpl  1666  sbequ2  1818  sbcof2  1859  sbequilem  1887  sbequ8  1896  euan  2139  mooran1  2155  eupickbi  2165  2exeu  2175  dimatis  2200  rexim  2638  r19.26  2671  r19.40  2699  rspcime  2931  rr19.28v  2960  elrab3t  2975  eueq3dc  2994  mosubt  2997  reu6  3009  sbc2iegf  3116  sbcralt  3122  sbcrext  3123  rmob  3139  csbiebt  3181  ssab2  3326  difdif  3348  uneqin  3476  indifdir  3481  undif3ss  3486  rexm  3613  eqifdc  3663  ifandc  3667  ifnebibdc  3672  difsn  3836  opprc1  3910  unissel  3948  ssmin  3973  abssexg  4300  undifexmid  4311  pwntru  4317  exmidundif  4324  exmidundifim  4325  opelopabsb  4383  elopabran  4407  sess1  4463  ordelord  4507  onin  4512  suctr  4547  abnexg  4572  ifexg  4611  ordtriexmidlem  4646  ordtri2or2exmid  4698  ontri2orexmidim  4699  tfi  4709  peano1  4721  peano2  4722  nnpredcl  4750  0nelxp  4782  0nelelxp  4783  brab2a  4808  mosubopt  4820  posng  4827  opabssxp  4829  ideqg  4911  relssres  5081  trin2  5159  dminss  5182  iota4an  5338  iota2  5347  iotam  5349  fununfun  5404  fun11uni  5431  imadiflem  5440  funimaexg  5445  fneq12  5454  fvelrnb  5729  dffo4  5830  ffnfv  5840  ffvresb  5845  fmptco  5848  fcoconst  5853  funopsn  5865  fndmexb  5912  fcof1  5962  isotr  5995  isopolem  6001  f1oiso  6005  acexmidlemcase  6053  ovprc1  6095  fnoprabg  6162  elovmporab  6262  elovmporab1w  6263  uchoice  6344  op1steq  6386  dmmpog  6418  1stconst  6430  f1o2ndf1  6437  suppfnss  6470  suppssfvg  6476  brtpos2  6495  tpostpos  6508  tposf12  6513  smores  6536  tfrlemi1  6576  tfr1onlembfn  6588  tfri1dALT  6595  tfrcllembfn  6601  freceq1  6636  freceq2  6637  frectfr  6644  omv2  6711  omsuc  6718  nnsucelsuc  6737  nntri3  6743  nnaordi  6754  nnmordi  6762  nnm00  6776  ecexr  6785  ertr  6795  swoer  6808  erth  6826  ecelqsdm  6852  iinerm  6854  ecinxp  6857  erovlem  6874  pmresg  6923  resixp  6981  elixpsn  6983  mapsnf1o  6985  dom3  7028  modom  7074  mapdom1g  7113  ssenen  7118  phpelm  7134  finexdc  7173  exmidpweq  7182  nnwetri  7189  fiintim  7204  infidc  7214  suppeqfsuppbi  7261  ssfii  7274  fiss  7277  dcfi  7281  2omap  7282  supubti  7303  supisoex  7313  ordiso2  7339  inl11  7369  omp1eomlem  7398  nnnninf  7430  nninfisol  7437  ctssexmid  7454  ismkvnex  7459  omniwomnimkv  7471  nninfwlpor  7478  nninfwlpoim  7483  nninfinfwlpo  7484  en2eleq  7511  en2other2  7512  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  acnrcl  7521  exmidaclem  7528  djuen  7531  djudoml  7539  netap  7584  2omotaplemst  7588  exmidapne  7590  cc1  7595  acnccim  7602  dmaddpqlem  7708  distrnqg  7718  ltanqi  7733  ltmnqi  7734  ltaddnq  7738  ltrnqg  7751  ltnnnq  7754  enq0sym  7763  addnq0mo  7778  mulnq0mo  7779  addnnnq0  7780  distrnq0  7790  prarloclemn  7830  prarloc  7834  ltdfpr  7837  genplt2i  7841  addnqprl  7860  addnqpru  7861  nqprl  7882  appdivnq  7894  1idprl  7921  1idpru  7922  ltexpri  7944  recexpr  7969  cauappcvgprlemdisj  7982  archrecpr  7995  addsrmo  8074  mulsrmo  8075  addsrpr  8076  mulsrpr  8077  0idsr  8098  1idsr  8099  archsr  8113  prsradd  8117  prsrlt  8118  caucvgsr  8133  map2psrprg  8136  elrealeu  8160  muladd11r  8445  negeu  8480  pncan  8495  pncan3  8497  negsub  8537  addid0  8662  addeq0  8666  posdif  8746  ltnegcon1  8754  subge0  8766  suble0  8767  lesub0  8770  reapval  8867  reapneg  8888  ap0gt0  8931  aprcl  8937  lt0ap0  8939  recextlem1  8942  recapb  8962  div0ap  8993  recrecap  9000  rec11ap  9001  recgt0  9141  mulgt1  9154  lerec2  9180  recp1lt1  9190  recreclt  9191  ledivp1  9194  negiso  9246  nnsub  9293  avglt1  9494  nnrecl  9511  nnnn0addcl  9543  elnn0nn  9555  fcdmnn0fsuppg  9568  nn0ge2m1nn  9577  zaddcl  9634  eluzmn  9878  eluzadd  9901  infregelbex  9948  divfnzn  9971  qaddcl  9985  qreccl  9992  cnref1o  10001  ge0p1rp  10036  divlt1lt  10075  divle1le  10076  addlelt  10119  xrre3  10174  xltnegi  10187  xaddval  10197  xaddcom  10213  xnegdi  10220  xposdif  10234  ixxssixx  10254  iccshftr  10346  iccshftl  10348  iccdil  10350  icccntr  10352  zltaddlt1le  10360  elfz2  10368  peano2fzr  10391  fzdcel  10394  fzsplit2  10404  fzaddel  10414  fzrev2  10441  fzrev2i  10442  fzrev3  10443  elfz1b  10446  fseq1p1m1  10450  uzsubfz0  10485  fzosubel3  10563  eluzgtdifelfzo  10564  fzofzp1b  10595  elfzomelpfzo  10598  exfzdc  10608  fvinim0ffz  10609  zsupcllemex  10612  infssuzcldc  10617  exbtwnzlemshrink  10632  qbtwnz  10635  qbtwnxr  10641  ico0  10645  elicore  10650  xqltnle  10651  apbtwnz  10658  flqge  10666  flqlt  10667  flqltnz  10671  flqbi2  10675  flqaddz  10681  flqmulnn0  10683  intfracq  10706  flqdiv  10707  q0mod  10741  q1mod  10742  mulp1mod1  10751  q2txmodxeq0  10770  modfzo0difsn  10781  frec2uzuzd  10788  frec2uzltd  10789  frec2uzrand  10791  uzennn  10822  seqfveq2g  10863  seq3split  10874  seqsplitg  10875  seq3caopr  10881  seqcaoprg  10882  seqf1oglem2  10906  seqf1og  10907  exp3vallem  10926  exp3val  10927  expnnval  10928  exp1  10931  expcl2lemap  10937  rpexpcl  10944  expnegzap  10959  mulexp  10964  mulexpzap  10965  leexp2r  10979  leexp1a  10980  sq11  10998  subsq  11032  binom2  11037  binom3  11043  zesq  11045  bernneq  11047  sq11ap  11094  zzlesq  11095  mulsubdivbinom2ap  11098  apexp1  11105  facwordi  11127  facubnd  11132  facavg  11133  bcval  11136  bcval5  11150  hashennn  11168  fihashf1rn  11176  fseq1hash  11190  hashdifsn  11209  hashdifpr  11210  hashxp  11216  hashmap  11217  fiubz  11221  fiubnn  11222  fnfz0hash  11224  ffzo0hash  11226  ssenneg  11229  hashfibclem  11231  hash2en  11240  wrdval  11252  ffz0iswrdnn0  11276  wrdsymb0  11282  ccatsymb  11315  ccatval21sw  11318  lswccatn0lsw  11324  ccatalpha  11326  ccatrcl1  11327  s111  11344  ccat1st1st  11354  lswccats1fst  11357  swrdlen2  11379  swrdfv2  11380  swrdsbslen  11383  swrds1  11385  ccatswrd  11387  pfxval  11391  pfxclg  11395  pfxmpt  11397  pfxid  11403  pfxfv0  11409  pfxtrcfv0  11411  pfxfvlsw  11412  pfxeq  11413  ccatpfx  11418  swrdpfx  11424  lenrevpfxcctswrd  11429  wrdeqs1cat  11437  cats1un  11438  swrdccatin1  11442  pfxccatin12lem2a  11444  pfxccatin12lem1  11445  pfxccatin12lem3  11449  pfxccatin12  11450  swrdccat  11452  pfxccat3a  11455  swrdccat3blem  11456  swrdccat3b  11457  reuccatpfxs1lem  11463  reuccatpfxs1  11464  s2cl  11502  s2fv0g  11504  shftfvalg  11528  ovshftex  11529  shftdm  11532  shftfib  11533  shftval  11535  shftf  11540  crre  11567  cjexp  11603  cjreim2  11614  uzin2  11697  rexuz3  11700  resqrexlemgt0  11730  resqrex  11736  sqrtgt0  11744  sqrtsq  11754  sqrtmsq  11755  absrpclap  11771  absext  11773  absmul  11779  absid  11781  absexp  11789  nn0abscl  11795  abslt  11798  absle  11799  recvalap  11807  abstri  11814  caubnd2  11827  qdenre  11912  maxabsle  11914  maxabslemval  11918  maxcl  11920  rexanre  11930  min1inf  11942  minabs  11946  minclpr  11947  mul0inf  11951  mingeb  11952  xrmaxiflemcl  11955  xrnegiso  11972  climconst2  12001  climmpt  12010  climres  12013  climcaucn  12061  sumeq1  12065  summodclem2a  12092  isumz  12100  fisumss  12103  fsumzcl2  12116  sumsnf  12120  isumclim3  12134  fsum2dlemstep  12145  fisumcom2  12149  fsumconst  12165  cvgcmpub  12187  binom  12195  binom1p  12196  binom1dif  12198  bcxmas  12200  divcnv  12208  geo2lim  12227  geoisum  12228  geoisumr  12229  geoisum1  12230  mertenslemi1  12246  mertensabs  12248  prod1dc  12297  fprodconst  12331  fprodcom2fi  12337  efcllem  12370  efcj  12384  efadd  12386  efexp  12393  efgt1p2  12406  tanvalap  12419  tanval2ap  12424  tanval3ap  12425  sinadd  12447  cosadd  12448  dvdsdc  12509  iddvdsexp  12526  dvdsadd  12547  dvds1  12564  odd2np1  12584  oddm1even  12586  m1exp1  12612  divalglemnn  12629  fldivndvdslt  12648  flodddiv4lt  12649  bitsp1  12662  bitsmod  12667  bitsfi  12668  bitscmp  12669  bitsinv1lem  12672  dvdsbnd  12677  gcdnncl  12688  zeqzmulgcd  12691  gcdneg  12703  modgcd  12712  bezoutlemex  12722  bezoutlemeu  12728  dfgcd3  12731  gcdzeq  12743  dvdssq  12752  algrf  12767  eucalgval2  12775  eucalgcvga  12780  lcmval  12785  gcddvdslcm  12795  lcmneg  12796  coprmgcdb  12810  qredeu  12819  divgcdcoprm0  12823  divgcdcoprmex  12824  cncongr1  12825  cncongr2  12826  cncongrcoprm  12828  prmind2  12842  dvdsnprmd  12847  exprmfct  12860  isprm6  12869  pw2dvdslemn  12887  oddpwdclemdc  12895  sqrt2irraplemnn  12901  divnumden  12918  divdenle  12919  nn0sqrtelqelz  12928  phivalfi  12934  crth  12946  eulerth  12955  prmdivdiv  12959  reumodprminv  12976  nnnn0modprm0  12978  nnoddn2prmb  12985  pcval  13019  pcidlem  13046  pcid  13047  pcneg  13048  pc2dvds  13053  pcz  13055  pcprod  13069  prmpwdvds  13078  4sqexercise1  13121  2expltfac  13162  ballotfilemfval  13173  ballotfilemefi  13181  ballotfilemodife  13184  ballotfilem4  13185  ballotfilemsval  13196  ballotfilemieq  13204  ballotfilemrv  13207  ballotfilemrinv0  13220  xpct  13231  znnen  13233  ennnfonelemg  13238  ennnfone  13260  ctinfom  13263  ctinf  13265  ssomct  13280  isstruct2im  13306  isstruct2r  13307  setsvalg  13326  setsslnid  13348  ressvalsets  13361  ressex  13362  2strbasg  13417  2stropg  13418  2strbas1g  13420  ressmulrg  13442  ressscag  13480  ressvscag  13481  ressipg  13482  restval  13542  restid2  13545  qusex  13589  fnpr2o  13603  xpsfval  13612  intopsn  13630  mgmidmo  13635  lidrididd  13645  ismnddef  13679  mndinvmod  13706  imasmnd2  13707  ismhm  13716  mhmex  13717  insubm  13740  dfgrp2  13782  grpsubval  13801  grpinvinv  13822  grpsubrcan  13836  grpsubadd  13843  grpaddsubass  13845  grpsubsub4  13848  grppnpcan2  13849  grpnpncan  13850  grpnpncan0  13851  grpnnncan2  13852  dfgrp3m  13854  dfgrp3me  13855  imasgrp2  13863  mhmmnd  13869  mulgfvalg  13874  mulgval  13875  mulgfng  13877  mulg1  13882  mulgnnp1  13883  mulgnndir  13904  mulgass  13912  mulgmodid  13914  issubg2m  13942  grpissubg  13947  isnsg  13955  isnsg3  13960  0nsg  13967  eqgfval  13975  eqger  13977  eqgen  13980  eqgcpbl  13981  quseccl  13986  isghm  13996  kerf1ghm  14027  conjghm  14029  conjsubg  14030  abladdsub  14068  ablpncan3  14070  ablsubsub23  14078  invghm  14082  subgabl  14085  prdsex  14114  xpsval  14143  pwsval  14146  mgpress  14170  rngdi  14179  rnglz  14184  imasrng  14195  srgmulgass  14232  srgrmhm  14237  isring  14243  ringo2times  14271  ringrng  14279  ringlz  14286  imasring  14307  opprrng  14320  opprrngbg  14321  opprring  14322  mulgass3  14329  dvdsrd  14339  dvdsrneg  14348  unitnegcl  14375  dvrvald  14379  dvrid  14382  dvr1  14383  dvrass  14384  dvrdir  14388  ringinvdv  14390  rhmex  14402  isrim0  14406  rhmval  14418  rhmdvdsr  14420  rhmopp  14421  elrhmunit  14422  rhmunitinv  14423  isnzr2  14429  ringelnzr  14432  issubrng2  14456  issubrg2  14487  ringunitap  14531  aprap  14536  aprnzr  14537  opprdrng  14558  lmodvs1  14590  lmod0vs  14595  lmodvs0  14596  lmodvsmmulgdi  14597  lmodfopne  14600  lmodvneg1  14604  lss1  14636  islss3  14653  lsslss  14655  lss1d  14657  lspf  14663  lspsn  14690  lspsnneg  14694  sraval  14711  sraring  14723  qus1  14800  qusrhm  14802  cnfldui  14863  dvdsrzring  14877  mulgghm2  14882  mulgrhm  14883  znval  14910  znf1o  14925  psrbagfi  14949  psrbagconcl  14953  psrplusgg  14959  mplgrpfi  14987  eltg2b  15045  difopn  15099  ntrcls0  15122  neii1  15138  restbasg  15159  resttopon  15162  restuni2  15168  cnrest2r  15228  tx1cn  15260  txcnp  15262  txcn  15266  txswaphmeo  15312  psmettri  15321  xmeteq0  15350  xmettri  15363  metrtri  15368  ssblex  15422  xmeter  15427  isxms2  15443  cnbl0  15525  cnblcld  15526  reopnap  15537  tgioo  15545  addcncntoplem  15552  expcn  15560  rescncf  15572  cncfcdm  15573  mulc1cncf  15580  cncfcncntop  15584  addccncf  15591  cdivcncfap  15595  negcncf  15596  cnopnap  15602  suplociccex  15616  hoverlt1  15640  hovergt0  15641  dich0  15643  limccl  15650  ellimc3apf  15651  cnplimcim  15658  limccnp2lem  15667  reldvg  15670  dvbsssg  15677  dvcjbr  15699  dvcj  15700  dvfre  15701  dvrecap  15704  dvef  15718  plyaddcl  15745  plymulcl  15746  plysubcl  15747  plyrecj  15754  reeff1olem  15762  pilem3  15774  ptolemy  15815  rplogcl  15870  rpcxpef  15885  cxprec  15901  rpcxproot  15905  rplogb1  15939  logbgt0b  15957  logbgcd1irr  15958  binom4  15970  wilthlem1  15974  sgmnncl  15982  dvdsppwf1o  15983  mersenne  15991  lgslem4  16002  lgsval  16003  lgsval2lem  16009  lgsval4a  16021  lgsdir2lem3  16029  lgsdir2  16032  lgsne0  16037  lgsprme0  16041  lgsmulsqcoprm  16045  gausslemma2dlem0a  16048  gausslemma2dlem1a  16057  2lgslem1b  16088  2lgslem2  16091  2lgsoddprm  16112  struct2slots2dom  16159  structvtxval  16160  structiedg0val  16161  struct2griedg  16167  edgstruct  16185  uhgr0vb  16205  incistruhgr  16211  umgrvad2edg  16332  uspgredg2vlem  16341  uspgredg2v  16342  usgredg2v  16345  ushgredgedg  16347  ushgredgedgloop  16349  usgr0vb  16354  uhgr0vusgr  16359  edg0usgr  16368  subupgr  16394  upgrspanop  16404  umgrspanop  16405  usgrspanop  16406  vtxdgfval  16409  wksfval  16443  wlkpropg  16445  uspgr2wlkeq2  16487  uspgr2wlkeqi  16488  upgr2wlkdc  16498  trlsex  16508  clwwlkccatlem  16521  clwwlkng  16526  clwwlkext2edg  16543  clwwlknccat  16544  umgr2cwwkdifex  16546  clwwlknonel  16553  clwwlknonccat  16554  clwwlknonex2lem2  16559  clwwlknun  16562  eupthsg  16566  eupth2lem3lem6fi  16592  bj-nnan  16634  bj-indind  16828  bj-omtrans  16852  bj-inf2vnlem1  16866  sscoll2  16884  pw1map  16895  pwtrufal  16897  sssneq  16902  pw1nct  16903  exmidnotnotr  16905  nninfsellemsuc  16916  nninfomnilem  16922  nnnninfex  16926  exmidsbthrlem  16928  qdencn  16933  trilpo  16953  trirec0  16954  apdiff  16958  iswomninnlem  16960  iswomni0  16962  redcwlpo  16966  redc0  16968  reap0  16969  cndcap  16970  dceqnconst  16972  dcapnconst  16973  neapmkv  16980  neap0mkv  16981