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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-ia1 106

This theorem is used by:  simpli  111  simpld  112  imp  124  adantrd  279  iba  300  pm3.41  331  pm4.45im  334  anim12  344  pm4.71  393  adantlr  481  adantrr  483  adantllr  485  adantlrr  487  adantrlr  489  adantrrr  491  simplll  539  simplrl  541  simprll  543  simprrl  545  anabs1  578  jcab  611  pm4.38  613  pm5.21  707  ioran  764  pm3.14  765  pm4.44  791  ordi  828  pm4.39  834  animorl  835  animorlr  837  pm5.16  840  pm5.54dc  930  intnanr  942  intnanrd  944  dcan  946  dedlema  982  dedlemb  983  pm4.42r  984  prlem2  987  ifpdc  992  dfifp2dc  994  simp1l  1052  simp2l  1054  simp3l  1056  3anandis  1388  xordc1  1442  anxordi  1449  falantru  1452  19.26  1534  exsimpl  1670  sbequ2  1822  sbcof2  1863  sbequilem  1891  sbequ8  1900  euan  2143  mooran1  2159  eupickbi  2169  2exeu  2179  dimatis  2204  rexim  2644  r19.26  2677  r19.40  2705  rspcime  2937  rr19.28v  2966  elrab3t  2981  eueq3dc  3000  mosubt  3003  reu6  3015  sbc2iegf  3122  sbcralt  3128  sbcrext  3129  rmob  3145  csbiebt  3187  ssab2  3332  difdif  3354  uneqin  3482  indifdir  3487  undif3ss  3492  abanssl  3501  rexm  3627  eqifdc  3677  ifandc  3681  ifnebibdc  3686  difsn  3852  opprc1  3926  unissel  3964  ssmin  3989  abssexg  4319  undifexmid  4330  pwntru  4336  exmidundif  4343  exmidundifim  4344  opelopabsb  4402  elopabran  4426  sess1  4482  ordelord  4526  onin  4531  suctr  4566  abnexg  4592  ifexg  4631  ordtriexmidlem  4666  ordtri2or2exmid  4718  ontri2orexmidim  4719  tfi  4729  peano1  4741  peano2  4742  nnpredcl  4770  0nelxp  4802  0nelelxp  4803  brab2a  4828  mosubopt  4840  posng  4847  opabssxp  4849  ideqg  4931  relssres  5101  trin2  5179  dminss  5202  iota4an  5358  iota2  5367  iotam  5369  fununfun  5424  fun11uni  5451  imadiflem  5460  funimaexg  5465  fneq12  5474  fvelrnb  5750  dffo4  5856  ffnfv  5866  ffvresb  5871  fmptco  5874  fcoconst  5879  funopsn  5891  fndmexb  5938  mptmex  5945  fcof1  5989  isotr  6022  isopolem  6028  f1oiso  6032  acexmidlemcase  6080  ovprc1  6122  fnoprabg  6189  elovmporab  6289  elovmporab1w  6290  uchoice  6371  op1steq  6413  dmmpog  6445  1stconst  6457  f1o2ndf1  6464  suppfnss  6497  suppssfvg  6503  brtpos2  6522  tpostpos  6535  tposf12  6540  smores  6563  tfrlemi1  6603  tfr1onlembfn  6615  tfri1dALT  6622  tfrcllembfn  6628  freceq1  6663  freceq2  6664  frectfr  6671  omv2  6738  omsuc  6745  nnsucelsuc  6764  nntri3  6770  nnaordi  6781  nnmordi  6789  nnm00  6803  ecexr  6812  ertr  6822  swoer  6835  erth  6853  ecelqsdm  6879  iinerm  6881  ecinxp  6884  erovlem  6901  pmresg  6957  resixp  7015  elixpsn  7017  mapsnf1o  7019  dom3  7062  modom  7108  mapdom1g  7147  ssenen  7152  phpelm  7168  finexdc  7207  exmidpweq  7216  nnwetri  7223  fiintim  7238  infidc  7248  suppeqfsuppbi  7295  ssfii  7308  fiss  7311  dcfi  7315  2omap  7318  supubti  7339  supisoex  7349  ordiso2  7375  inl11  7405  omp1eomlem  7434  nnnninf  7466  nninfisol  7473  ctssexmid  7490  ismkvnex  7495  omniwomnimkv  7507  nninfwlpor  7514  nninfwlpoim  7519  nninfinfwlpo  7520  en2eleq  7547  en2other2  7548  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  acnrcl  7557  exmidaclem  7564  djuen  7567  djudoml  7575  netap  7620  2omotaplemst  7624  exmidapne  7626  cc1  7631  acnccim  7638  dmaddpqlem  7744  distrnqg  7754  ltanqi  7769  ltmnqi  7770  ltaddnq  7774  ltrnqg  7787  ltnnnq  7790  enq0sym  7799  addnq0mo  7814  mulnq0mo  7815  addnnnq0  7816  distrnq0  7826  prarloclemn  7866  prarloc  7870  ltdfpr  7873  genplt2i  7877  addnqprl  7896  addnqpru  7897  nqprl  7918  appdivnq  7930  1idprl  7957  1idpru  7958  ltexpri  7980  recexpr  8005  cauappcvgprlemdisj  8018  archrecpr  8031  addsrmo  8110  mulsrmo  8111  addsrpr  8112  mulsrpr  8113  0idsr  8134  1idsr  8135  archsr  8149  prsradd  8153  prsrlt  8154  caucvgsr  8169  map2psrprg  8172  elrealeu  8196  muladd11r  8482  negeu  8517  pncan  8532  pncan3  8534  negsub  8574  addid0  8699  addeq0  8703  posdif  8783  ltnegcon1  8791  subge0  8803  suble0  8804  lesub0  8807  reapval  8904  reapneg  8925  ap0gt0  8968  aprcl  8974  lt0ap0  8976  recextlem1  8979  recapb  9001  div0ap  9032  recrecap  9039  rec11ap  9040  recgt0  9180  mulgt1  9193  lerec2  9219  recp1lt1  9229  recreclt  9230  ledivp1  9233  negiso  9285  nnsub  9343  avglt1  9544  nnrecl  9561  nnnn0addcl  9593  elnn0nn  9605  fcdmnn0fsuppg  9618  nn0ge2m1nn  9627  zaddcl  9684  eluzmn  9928  eluzadd  9951  infregelbex  9998  divfnzn  10021  qaddcl  10035  qreccl  10042  cnref1o  10051  ge0p1rp  10086  divlt1lt  10125  divle1le  10126  addlelt  10169  xrre3  10224  xltnegi  10237  xaddval  10247  xaddcom  10263  xnegdi  10270  xposdif  10284  ixxssixx  10304  iccshftr  10396  iccshftl  10398  iccdil  10400  icccntr  10402  zltaddlt1le  10410  elfz2  10418  peano2fzr  10441  fzdcel  10444  fzsplit2  10455  fzaddel  10465  fzrev2  10492  fzrev2i  10493  fzrev3  10494  elfz1b  10497  fseq1p1m1  10501  uzsubfz0  10536  fzosubel3  10614  eluzgtdifelfzo  10615  fzofzp1b  10646  elfzomelpfzo  10649  exfzdc  10659  fvinim0ffz  10660  zsupcllemex  10663  infssuzcldc  10668  exbtwnzlemshrink  10683  qbtwnz  10686  qbtwnxr  10692  ico0  10696  elicore  10701  xqltnle  10702  apbtwnz  10709  flqge  10717  flqlt  10718  flqltnz  10722  flqbi2  10726  flqaddz  10732  flqmulnn0  10734  intfracq  10757  flqdiv  10758  q0mod  10792  q1mod  10793  mulp1mod1  10802  q2txmodxeq0  10821  modfzo0difsn  10832  frec2uzuzd  10839  frec2uzltd  10840  frec2uzrand  10842  uzennn  10873  seqfveq2g  10914  seq3split  10925  seqsplitg  10926  seq3caopr  10932  seqcaoprg  10933  seqf1oglem2  10957  seqf1og  10958  exp3vallem  10977  exp3val  10978  expnnval  10979  exp1  10982  expcl2lemap  10988  rpexpcl  10995  expnegzap  11010  mulexp  11015  mulexpzap  11016  leexp2r  11030  leexp1a  11031  sq11  11049  subsq  11083  binom2  11088  binom3  11094  zesq  11096  bernneq  11098  sq11ap  11145  zzlesq  11146  mulsubdivbinom2ap  11149  apexp1  11156  facwordi  11178  facubnd  11183  facavg  11184  bcval  11187  bcval5  11201  hashennn  11219  fihashf1rn  11227  fseq1hash  11241  hashdifsn  11260  hashdifpr  11261  hashxp  11267  hashmap  11268  fiubz  11272  fiubnn  11273  fnfz0hash  11275  ffzo0hash  11277  ssenneg  11280  hashfibclem  11282  hashf1  11287  hash2en  11295  wrdval  11307  ffz0iswrdnn0  11331  wrdsymb0  11337  ccatsymb  11370  ccatval21sw  11373  lswccatn0lsw  11379  ccatalpha  11381  ccatrcl1  11382  s111  11399  ccat1st1st  11409  lswccats1fst  11412  swrdlen2  11434  swrdfv2  11435  swrdsbslen  11438  swrds1  11440  ccatswrd  11442  pfxval  11446  pfxclg  11450  pfxmpt  11452  pfxid  11458  pfxfv0  11464  pfxtrcfv0  11466  pfxfvlsw  11467  pfxeq  11468  ccatpfx  11473  swrdpfx  11479  lenrevpfxcctswrd  11484  wrdeqs1cat  11492  cats1un  11493  swrdccatin1  11497  pfxccatin12lem2a  11499  pfxccatin12lem1  11500  pfxccatin12lem3  11504  pfxccatin12  11505  swrdccat  11507  pfxccat3a  11510  swrdccat3blem  11511  swrdccat3b  11512  reuccatpfxs1lem  11518  reuccatpfxs1  11519  s2cl  11557  s2fv0g  11559  shftfvalg  11583  ovshftex  11584  shftdm  11587  shftfib  11588  shftval  11590  shftf  11595  crre  11622  cjexp  11658  cjreim2  11670  uzin2  11753  rexuz3  11756  resqrexlemgt0  11786  resqrex  11792  sqrtgt0  11800  sqrtsq  11810  sqrtmsq  11811  absrpclap  11827  absext  11829  absmul  11835  absid  11837  absexp  11845  nn0abscl  11851  abslt  11854  absle  11855  recvalap  11863  abstri  11870  caubnd2  11883  qdenre  11968  maxabsle  11970  maxabslemval  11974  maxcl  11976  rexanre  11986  min1inf  11998  minabs  12002  minclpr  12003  mul0inf  12007  mingeb  12008  xrmaxiflemcl  12011  xrnegiso  12028  climconst2  12057  climmpt  12066  climres  12069  climcaucn  12117  sumeq1  12121  summodclem2a  12148  isumz  12156  fisumss  12159  fsumzcl2  12172  sumsnf  12176  isumclim3  12190  fsum2dlemstep  12201  fisumcom2  12205  fsumconst  12221  cvgcmpub  12243  binom  12251  binom1p  12252  binom1dif  12254  bcxmas  12256  divcnv  12264  geo2lim  12283  geoisum  12284  geoisumr  12285  geoisum1  12286  mertenslemi1  12302  mertensabs  12304  prod1dc  12353  fprodconst  12387  fprodcom2fi  12393  efcllem  12426  efcj  12440  efadd  12442  efexp  12449  efgt1p2  12462  tanvalap  12475  tanval2ap  12480  tanval3ap  12481  sinadd  12503  cosadd  12504  dvdsdc  12565  iddvdsexp  12582  dvdsadd  12603  dvds1  12620  odd2np1  12640  oddm1even  12642  m1exp1  12668  divalglemnn  12685  fldivndvdslt  12704  flodddiv4lt  12705  bitsp1  12718  bitsmod  12723  bitsfi  12724  bitscmp  12725  bitsinv1lem  12728  dvdsbnd  12733  gcdnncl  12744  zeqzmulgcd  12747  gcdneg  12759  modgcd  12768  bezoutlemex  12778  bezoutlemeu  12784  dfgcd3  12787  gcdzeq  12799  dvdssq  12808  algrf  12823  eucalgval2  12831  eucalgcvga  12836  lcmval  12841  gcddvdslcm  12851  lcmneg  12852  coprmgcdb  12866  qredeu  12875  divgcdcoprm0  12879  divgcdcoprmex  12880  cncongr1  12881  cncongr2  12882  cncongrcoprm  12884  prmind2  12898  dvdsnprmd  12903  exprmfct  12916  isprm6  12925  pw2dvdslemn  12943  oddpwdclemdc  12951  sqrt2irraplemnn  12957  divnumden  12974  divdenle  12975  nn0sqrtelqelz  12984  phivalfi  12990  crth  13002  eulerth  13011  prmdivdiv  13015  reumodprminv  13032  nnnn0modprm0  13034  nnoddn2prmb  13041  pcval  13075  pcidlem  13102  pcid  13103  pcneg  13104  pc2dvds  13109  pcz  13111  pcprod  13125  prmpwdvds  13134  4sqexercise1  13177  2expltfac  13218  ballotfilemfval  13229  ballotfilemefi  13237  ballotfilemodife  13240  ballotfilem4  13241  ballotfilemsval  13252  ballotfilemieq  13260  ballotfilemrv  13263  ballotfilemrinv0  13276  xpct  13287  znnen  13289  ennnfonelemg  13294  ennnfone  13316  ctinfom  13319  ctinf  13321  ssomct  13336  isstruct2im  13362  isstruct2r  13363  setsvalg  13382  setsslnid  13404  ressvalsets  13418  ressex  13419  2strbasg  13474  2stropg  13475  2strbas1g  13477  ressmulrg  13499  ressscag  13537  ressvscag  13538  ressipg  13539  restval  13599  restid2  13602  qusex  13646  fnpr2o  13660  xpsfval  13669  intopsn  13687  mgmidmo  13692  lidrididd  13702  ismnddef  13731  mndinvmod  13758  imasmnd2  13759  ismhm  13768  mhmex  13769  insubm  13792  dfgrp2  13832  grpsubval  13851  grpinvinv  13872  grpsubrcan  13886  grpsubadd  13893  grpaddsubass  13895  grpsubsub4  13898  grppnpcan2  13899  grpnpncan  13900  grpnpncan0  13901  grpnnncan2  13902  dfgrp3m  13904  dfgrp3me  13905  imasgrp2  13913  mhmmnd  13919  mulgfvalg  13924  mulgval  13925  mulgfng  13927  mulg1  13932  mulgnnp1  13933  mulgnndir  13954  mulgass  13962  mulgmodid  13964  issubg2m  13992  grpissubg  13997  isnsg  14005  isnsg3  14010  0nsg  14017  eqgfval  14025  eqger  14027  eqgen  14030  eqgcpbl  14031  quseccl  14036  isghm  14046  kerf1ghm  14077  conjghm  14079  conjsubg  14080  abladdsub  14119  ablpncan3  14121  ablsubsub23  14129  invghm  14133  subgabl  14136  prdsex  14172  xpsval  14201  pwsval  14204  mgpress  14230  rngdi  14239  rnglz  14244  imasrng  14255  srgmulgass  14293  srgrmhm  14298  isring  14304  ringo2times  14333  ringrng  14341  ringlz  14348  imasring  14369  opprrng  14382  opprrngbg  14383  opprring  14384  mulgass3  14391  dvdsrd  14401  dvdsrneg  14410  unitnegcl  14437  dvrvald  14441  dvrid  14444  dvr1  14445  dvrass  14446  dvrdir  14450  ringinvdv  14452  rhmex  14464  isrim0  14468  rhmval  14480  rhmdvdsr  14482  rhmopp  14483  elrhmunit  14484  rhmunitinv  14485  isnzr2  14491  ringelnzr  14494  issubrng2  14518  issubrg2  14549  ringunitap  14593  aprap  14598  aprnzr  14599  opprdrng  14620  lmodvs1  14653  lmod0vs  14658  lmodvs0  14659  lmodvsmmulgdi  14660  lmodfopne  14663  lmodvneg1  14667  lss1  14699  islss3  14716  lsslss  14718  lss1d  14720  lspf  14726  lspsn  14753  lspsnneg  14757  sraval  14774  sraring  14786  qus1  14863  qusrhm  14865  cnfldui  14924  dvdsrzring  14938  mulgghm2  14943  mulgrhm  14944  znval  14971  znf1o  14986  assa2ass  15009  assa2ass2  15010  issubassa3  15012  assamulgscmlem2  15042  psrbagfi  15059  psrbagconcl  15063  psrplusgg  15069  mplgrpfi  15097  eltg2b  15155  difopn  15209  ntrcls0  15232  neii1  15248  restbasg  15269  resttopon  15272  restuni2  15278  cnrest2r  15338  tx1cn  15370  txcnp  15372  txcn  15376  txswaphmeo  15422  psmettri  15431  xmeteq0  15460  xmettri  15473  metrtri  15478  ssblex  15532  xmeter  15537  isxms2  15553  cnbl0  15635  cnblcld  15636  reopnap  15647  tgioo  15655  addcncntoplem  15662  expcn  15670  rescncf  15682  cncfcdm  15683  mulc1cncf  15690  cncfcncntop  15694  addccncf  15701  cdivcncfap  15705  negcncf  15706  cnopnap  15712  suplociccex  15726  hoverlt1  15750  hovergt0  15751  dich0  15753  limccl  15760  ellimc3apf  15761  cnplimcim  15768  limccnp2lem  15777  reldvg  15780  dvbsssg  15787  dvcjbr  15809  dvcj  15810  dvfre  15811  dvrecap  15814  dvef  15828  plyaddcl  15855  plymulcl  15856  plysubcl  15857  plyrecj  15864  reeff1olem  15872  pilem3  15884  ptolemy  15925  rplogcl  15980  rpcxpef  15996  cxprec  16012  rpcxproot  16016  rplogb1  16050  logbgt0b  16068  logbgcd1irr  16069  binom4  16081  birthdaylem1g  16087  wilthlem1  16094  sgmnncl  16102  dvdsppwf1o  16103  mersenne  16111  lgslem4  16122  lgsval  16123  lgsval2lem  16129  lgsval4a  16141  lgsdir2lem3  16149  lgsdir2  16152  lgsne0  16157  lgsprme0  16161  lgsmulsqcoprm  16165  gausslemma2dlem0a  16168  gausslemma2dlem1a  16177  2lgslem1b  16208  2lgslem2  16211  2lgsoddprm  16232  struct2slots2dom  16279  structvtxval  16280  structiedg0val  16281  struct2griedg  16287  edgstruct  16305  uhgr0vb  16325  incistruhgr  16331  umgrvad2edg  16452  uspgredg2vlem  16461  uspgredg2v  16462  usgredg2v  16465  ushgredgedg  16467  ushgredgedgloop  16469  usgr0vb  16474  uhgr0vusgr  16479  edg0usgr  16488  subupgr  16514  upgrspanop  16524  umgrspanop  16525  usgrspanop  16526  vtxdgfval  16529  wksfval  16563  wlkpropg  16565  uspgr2wlkeq2  16607  uspgr2wlkeqi  16608  upgr2wlkdc  16618  trlsex  16628  clwwlkccatlem  16641  clwwlkng  16646  clwwlkext2edg  16663  clwwlknccat  16664  umgr2cwwkdifex  16666  clwwlknonel  16673  clwwlknonccat  16674  clwwlknonex2lem2  16679  clwwlknun  16682  eupthsg  16686  eupth2lem3lem6fi  16712  dichmul0orlem7  16759  dichmul0or  16760  bj-nnan  16764  bj-indind  16958  bj-omtrans  16982  bj-inf2vnlem1  16996  sscoll2  17014  pw1map  17025  pwtrufal  17027  sssneq  17032  pw1nct  17033  exmidnotnotr  17036  nninfsellemsuc  17055  nninfomnilem  17061  nnnninfex  17065  exmidsbthrlem  17067  qdencn  17072  trilpo  17092  trirec0  17093  apdiff  17097  iswomninnlem  17099  iswomni0  17101  redcwlpo  17105  redc0  17107  reap0  17108  cndcap  17109  dceqnconst  17110  dcapnconst  17111  neapmkv  17118  neap0mkv  17119  als-no-surprise  17147