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  533  simplrl  535  simprll  537  simprrl  539  anabs1  572  jcab  605  pm4.38  607  pm5.21  700  ioran  757  pm3.14  758  pm4.44  784  ordi  821  pm4.39  827  animorl  828  animorlr  830  pm5.16  833  pm5.54dc  923  intnanr  935  intnanrd  937  dcan  939  dedlema  975  dedlemb  976  pm4.42r  977  prlem2  980  ifpdc  985  dfifp2dc  987  simp1l  1045  simp2l  1047  simp3l  1049  3anandis  1381  xordc1  1435  anxordi  1442  falantru  1445  19.26  1527  exsimpl  1663  sbequ2  1815  sbcof2  1856  sbequilem  1884  sbequ8  1893  euan  2134  mooran1  2150  eupickbi  2160  2exeu  2170  dimatis  2195  rexim  2624  r19.26  2657  r19.40  2685  rspcime  2914  rr19.28v  2943  elrab3t  2958  eueq3dc  2977  mosubt  2980  reu6  2992  sbc2iegf  3099  sbcralt  3105  sbcrext  3106  rmob  3122  csbiebt  3164  ssab2  3308  difdif  3329  uneqin  3455  indifdir  3460  undif3ss  3465  rexm  3591  eqifdc  3639  ifandc  3643  ifnebibdc  3648  difsn  3805  opprc1  3879  unissel  3917  ssmin  3942  abssexg  4266  undifexmid  4277  pwntru  4283  exmidundif  4290  exmidundifim  4291  opelopabsb  4348  elopabran  4372  sess1  4428  ordelord  4472  onin  4477  suctr  4512  abnexg  4537  ifexg  4576  ordtriexmidlem  4611  ordtri2or2exmid  4663  ontri2orexmidim  4664  tfi  4674  peano1  4686  peano2  4687  nnpredcl  4715  0nelxp  4747  0nelelxp  4748  brab2a  4772  mosubopt  4784  posng  4791  opabssxp  4793  ideqg  4873  relssres  5043  trin2  5120  dminss  5143  iota4an  5299  iota2  5308  iotam  5310  fununfun  5364  fun11uni  5391  imadiflem  5400  funimaexg  5405  fneq12  5414  fvelrnb  5681  dffo4  5783  ffnfv  5793  ffvresb  5798  fmptco  5801  fcoconst  5806  funopsn  5817  fcof1  5907  isotr  5940  isopolem  5946  f1oiso  5950  acexmidlemcase  5996  ovprc1  6038  fnoprabg  6105  elovmporab  6205  elovmporab1w  6206  uchoice  6283  op1steq  6325  dmmpog  6355  1stconst  6367  f1o2ndf1  6374  brtpos2  6397  tpostpos  6410  tposf12  6415  smores  6438  tfrlemi1  6478  tfr1onlembfn  6490  tfri1dALT  6497  tfrcllembfn  6503  freceq1  6538  freceq2  6539  frectfr  6546  omv2  6611  omsuc  6618  nnsucelsuc  6637  nntri3  6643  nnaordi  6654  nnmordi  6662  nnm00  6676  ecexr  6685  ertr  6695  swoer  6708  erth  6726  ecelqsdm  6752  iinerm  6754  ecinxp  6757  erovlem  6774  pmresg  6823  resixp  6880  elixpsn  6882  mapsnf1o  6884  dom3  6927  mapdom1g  7008  ssenen  7012  phpelm  7028  finexdc  7064  exmidpweq  7071  nnwetri  7078  fiintim  7093  infidc  7101  ssfii  7141  fiss  7144  dcfi  7148  supubti  7166  supisoex  7176  ordiso2  7202  inl11  7232  omp1eomlem  7261  nnnninf  7293  nninfisol  7300  ctssexmid  7317  ismkvnex  7322  omniwomnimkv  7334  nninfwlpor  7341  nninfwlpoim  7346  nninfinfwlpo  7347  en2eleq  7373  en2other2  7374  exmidfodomrlemr  7380  exmidfodomrlemrALT  7381  acnrcl  7383  exmidaclem  7390  djuen  7393  djudoml  7401  netap  7440  2omotaplemst  7444  exmidapne  7446  cc1  7451  acnccim  7458  dmaddpqlem  7564  distrnqg  7574  ltanqi  7589  ltmnqi  7590  ltaddnq  7594  ltrnqg  7607  ltnnnq  7610  enq0sym  7619  addnq0mo  7634  mulnq0mo  7635  addnnnq0  7636  distrnq0  7646  prarloclemn  7686  prarloc  7690  ltdfpr  7693  genplt2i  7697  addnqprl  7716  addnqpru  7717  nqprl  7738  appdivnq  7750  1idprl  7777  1idpru  7778  ltexpri  7800  recexpr  7825  cauappcvgprlemdisj  7838  archrecpr  7851  addsrmo  7930  mulsrmo  7931  addsrpr  7932  mulsrpr  7933  0idsr  7954  1idsr  7955  archsr  7969  prsradd  7973  prsrlt  7974  caucvgsr  7989  map2psrprg  7992  elrealeu  8016  muladd11r  8302  negeu  8337  pncan  8352  pncan3  8354  negsub  8394  addid0  8519  posdif  8602  ltnegcon1  8610  subge0  8622  suble0  8623  lesub0  8626  reapval  8723  reapneg  8744  ap0gt0  8787  aprcl  8793  lt0ap0  8795  recextlem1  8798  recapb  8818  div0ap  8849  recrecap  8856  rec11ap  8857  recgt0  8997  mulgt1  9010  lerec2  9036  recp1lt1  9046  recreclt  9047  ledivp1  9050  negiso  9102  nnsub  9149  avglt1  9350  nnrecl  9367  nnnn0addcl  9399  elnn0nn  9411  nn0ge2m1nn  9429  zaddcl  9486  eluzadd  9751  infregelbex  9793  divfnzn  9816  qaddcl  9830  qreccl  9837  cnref1o  9846  ge0p1rp  9881  divlt1lt  9920  divle1le  9921  addlelt  9964  xrre3  10018  xltnegi  10031  xaddval  10041  xaddcom  10057  xnegdi  10064  xposdif  10078  ixxssixx  10098  iccshftr  10190  iccshftl  10192  iccdil  10194  icccntr  10196  zltaddlt1le  10203  elfz2  10211  peano2fzr  10233  fzdcel  10236  fzsplit2  10246  fzaddel  10255  fzrev2  10281  fzrev2i  10282  fzrev3  10283  elfz1b  10286  fseq1p1m1  10290  uzsubfz0  10325  fzosubel3  10402  eluzgtdifelfzo  10403  fzofzp1b  10434  elfzomelpfzo  10437  exfzdc  10446  fvinim0ffz  10447  zsupcllemex  10450  infssuzcldc  10455  exbtwnzlemshrink  10468  qbtwnz  10471  qbtwnxr  10477  ico0  10481  elicore  10486  xqltnle  10487  apbtwnz  10494  flqge  10502  flqlt  10503  flqltnz  10507  flqbi2  10511  flqaddz  10517  flqmulnn0  10519  intfracq  10542  flqdiv  10543  q0mod  10577  q1mod  10578  mulp1mod1  10587  q2txmodxeq0  10606  modfzo0difsn  10617  frec2uzuzd  10624  frec2uzltd  10625  frec2uzrand  10627  uzennn  10658  seqfveq2g  10699  seq3split  10710  seqsplitg  10711  seq3caopr  10717  seqcaoprg  10718  seqf1oglem2  10742  seqf1og  10743  exp3vallem  10762  exp3val  10763  expnnval  10764  exp1  10767  expcl2lemap  10773  rpexpcl  10780  expnegzap  10795  mulexp  10800  mulexpzap  10801  leexp2r  10815  leexp1a  10816  sq11  10834  subsq  10868  binom2  10873  binom3  10879  zesq  10880  bernneq  10882  sq11ap  10929  zzlesq  10930  mulsubdivbinom2ap  10933  apexp1  10940  facwordi  10962  facubnd  10967  facavg  10968  bcval  10971  bcval5  10985  hashennn  11002  fihashf1rn  11010  fseq1hash  11023  hashdifsn  11041  hashdifpr  11042  hashxp  11048  fiubz  11051  fiubnn  11052  fnfz0hash  11054  ffzo0hash  11056  hash2en  11065  wrdval  11074  ffz0iswrdnn0  11098  wrdsymb0  11104  ccatsymb  11137  ccatval21sw  11140  lswccatn0lsw  11146  s111  11164  ccat1st1st  11172  lswccats1fst  11175  swrdlen2  11194  swrdfv2  11195  swrdsbslen  11198  swrds1  11200  ccatswrd  11202  pfxval  11206  pfxclg  11210  pfxmpt  11212  pfxid  11218  pfxfv0  11224  pfxtrcfv0  11226  pfxfvlsw  11227  pfxeq  11228  ccatpfx  11233  swrdpfx  11239  lenrevpfxcctswrd  11244  wrdeqs1cat  11252  cats1un  11253  swrdccatin1  11257  pfxccatin12lem2a  11259  pfxccatin12lem1  11260  pfxccatin12lem3  11264  pfxccatin12  11265  swrdccat  11267  pfxccat3a  11270  swrdccat3blem  11271  swrdccat3b  11272  reuccatpfxs1lem  11278  reuccatpfxs1  11279  s2cl  11317  s2fv0g  11319  shftfvalg  11329  ovshftex  11330  shftdm  11333  shftfib  11334  shftval  11336  shftf  11341  crre  11368  cjexp  11404  cjreim2  11415  uzin2  11498  rexuz3  11501  resqrexlemgt0  11531  resqrex  11537  sqrtgt0  11545  sqrtsq  11555  sqrtmsq  11556  absrpclap  11572  absext  11574  absmul  11580  absid  11582  absexp  11590  nn0abscl  11596  abslt  11599  absle  11600  recvalap  11608  abstri  11615  caubnd2  11628  qdenre  11713  maxabsle  11715  maxabslemval  11719  maxcl  11721  rexanre  11731  min1inf  11743  minabs  11747  minclpr  11748  mul0inf  11752  mingeb  11753  xrmaxiflemcl  11756  xrnegiso  11773  climconst2  11802  climmpt  11811  climres  11814  climcaucn  11862  sumeq1  11866  summodclem2a  11892  isumz  11900  fisumss  11903  fsumzcl2  11916  sumsnf  11920  isumclim3  11934  fsum2dlemstep  11945  fisumcom2  11949  fsumconst  11965  cvgcmpub  11987  binom  11995  binom1p  11996  binom1dif  11998  bcxmas  12000  divcnv  12008  geo2lim  12027  geoisum  12028  geoisumr  12029  geoisum1  12030  mertenslemi1  12046  mertensabs  12048  prod1dc  12097  fprodconst  12131  fprodcom2fi  12137  efcllem  12170  efcj  12184  efadd  12186  efexp  12193  efgt1p2  12206  tanvalap  12219  tanval2ap  12224  tanval3ap  12225  sinadd  12247  cosadd  12248  dvdsdc  12309  iddvdsexp  12326  dvdsadd  12347  dvds1  12364  odd2np1  12384  oddm1even  12386  m1exp1  12412  divalglemnn  12429  fldivndvdslt  12448  flodddiv4lt  12449  bitsp1  12462  bitsmod  12467  bitsfi  12468  bitscmp  12469  bitsinv1lem  12472  dvdsbnd  12477  gcdnncl  12488  zeqzmulgcd  12491  gcdneg  12503  modgcd  12512  bezoutlemex  12522  bezoutlemeu  12528  dfgcd3  12531  gcdzeq  12543  dvdssq  12552  algrf  12567  eucalgval2  12575  eucalgcvga  12580  lcmval  12585  gcddvdslcm  12595  lcmneg  12596  coprmgcdb  12610  qredeu  12619  divgcdcoprm0  12623  divgcdcoprmex  12624  cncongr1  12625  cncongr2  12626  cncongrcoprm  12628  prmind2  12642  dvdsnprmd  12647  exprmfct  12660  isprm6  12669  pw2dvdslemn  12687  oddpwdclemdc  12695  sqrt2irraplemnn  12701  divnumden  12718  divdenle  12719  nn0sqrtelqelz  12728  phivalfi  12734  crth  12746  eulerth  12755  prmdivdiv  12759  reumodprminv  12776  nnnn0modprm0  12778  nnoddn2prmb  12785  pcval  12819  pcidlem  12846  pcid  12847  pcneg  12848  pc2dvds  12853  pcz  12855  pcprod  12869  prmpwdvds  12878  4sqexercise1  12921  2expltfac  12962  xpct  12967  znnen  12969  ennnfonelemg  12974  ennnfone  12996  ctinfom  12999  ctinf  13001  ssomct  13016  isstruct2im  13042  isstruct2r  13043  setsvalg  13062  setsslnid  13084  ressvalsets  13097  ressex  13098  2strbasg  13153  2stropg  13154  2strbas1g  13156  ressmulrg  13178  ressscag  13216  ressvscag  13217  ressipg  13218  restval  13278  restid2  13281  prdsex  13302  pwsval  13324  qusex  13358  fnpr2o  13372  xpsfval  13381  xpsval  13385  intopsn  13400  mgmidmo  13405  lidrididd  13415  ismnddef  13451  mndinvmod  13478  imasmnd2  13485  ismhm  13494  mhmex  13495  insubm  13518  dfgrp2  13560  grpsubval  13579  grpinvinv  13600  grpsubrcan  13614  grpsubadd  13621  grpaddsubass  13623  grpsubsub4  13626  grppnpcan2  13627  grpnpncan  13628  grpnpncan0  13629  grpnnncan2  13630  dfgrp3m  13632  dfgrp3me  13633  imasgrp2  13647  mhmmnd  13653  mulgfvalg  13658  mulgval  13659  mulgfng  13661  mulg1  13666  mulgnnp1  13667  mulgnndir  13688  mulgass  13696  mulgmodid  13698  issubg2m  13726  grpissubg  13731  isnsg  13739  isnsg3  13744  0nsg  13751  eqgfval  13759  eqger  13761  eqgen  13764  eqgcpbl  13765  quseccl  13770  isghm  13780  kerf1ghm  13811  conjghm  13813  conjsubg  13814  abladdsub  13852  ablpncan3  13854  ablsubsub23  13862  invghm  13866  subgabl  13869  mgpress  13894  rngdi  13903  rnglz  13908  imasrng  13919  srgmulgass  13952  srgrmhm  13957  isring  13963  ringo2times  13991  ringrng  13999  ringlz  14006  imasring  14027  opprrng  14040  opprrngbg  14041  opprring  14042  mulgass3  14048  dvdsrd  14058  dvdsrneg  14067  unitnegcl  14094  dvrvald  14098  dvrid  14101  dvr1  14102  dvrass  14103  dvrdir  14107  ringinvdv  14109  rhmex  14121  isrim0  14125  rhmval  14137  rhmdvdsr  14139  rhmopp  14140  elrhmunit  14141  rhmunitinv  14142  isnzr2  14148  ringelnzr  14151  issubrng2  14174  issubrg2  14205  aprap  14250  lmodvs1  14280  lmod0vs  14285  lmodvs0  14286  lmodvsmmulgdi  14287  lmodfopne  14290  lmodvneg1  14294  lss1  14326  islss3  14343  lsslss  14345  lss1d  14347  lspf  14353  lspsn  14380  lspsnneg  14384  sraval  14401  sraring  14413  qus1  14490  qusrhm  14492  cnfldui  14553  dvdsrzring  14567  mulgghm2  14572  mulgrhm  14573  znval  14600  znf1o  14615  psrbagfi  14637  psrplusgg  14642  mplgrpfi  14670  eltg2b  14728  difopn  14782  ntrcls0  14805  neii1  14821  restbasg  14842  resttopon  14845  restuni2  14851  cnrest2r  14911  tx1cn  14943  txcnp  14945  txcn  14949  txswaphmeo  14995  psmettri  15004  xmeteq0  15033  xmettri  15046  metrtri  15051  ssblex  15105  xmeter  15110  isxms2  15126  cnbl0  15208  cnblcld  15209  reopnap  15220  tgioo  15228  addcncntoplem  15235  expcn  15243  rescncf  15255  cncfcdm  15256  mulc1cncf  15263  cncfcncntop  15267  addccncf  15274  cdivcncfap  15278  negcncf  15279  cnopnap  15285  suplociccex  15299  hoverlt1  15323  hovergt0  15324  dich0  15326  limccl  15333  ellimc3apf  15334  cnplimcim  15341  limccnp2lem  15350  reldvg  15353  dvbsssg  15360  dvcjbr  15382  dvcj  15383  dvfre  15384  dvrecap  15387  dvef  15401  plyaddcl  15428  plymulcl  15429  plysubcl  15430  plyrecj  15437  reeff1olem  15445  pilem3  15457  ptolemy  15498  rplogcl  15553  rpcxpef  15568  cxprec  15584  rpcxproot  15588  rplogb1  15622  logbgt0b  15640  logbgcd1irr  15641  binom4  15653  wilthlem1  15654  sgmnncl  15662  dvdsppwf1o  15663  mersenne  15671  lgslem4  15682  lgsval  15683  lgsval2lem  15689  lgsval4a  15701  lgsdir2lem3  15709  lgsdir2  15712  lgsne0  15717  lgsprme0  15721  lgsmulsqcoprm  15725  gausslemma2dlem0a  15728  gausslemma2dlem1a  15737  2lgslem1b  15768  2lgslem2  15771  2lgsoddprm  15792  struct2slots2dom  15839  structvtxval  15840  structiedg0val  15841  struct2griedg  15847  edgstruct  15864  uhgr0vb  15884  incistruhgr  15890  umgrvad2edg  16009  uspgredg2vlem  16018  uspgredg2v  16019  usgredg2v  16022  ushgredgedg  16024  ushgredgedgloop  16026  wksfval  16035  wlkpropg  16037  uspgr2wlkeq2  16077  uspgr2wlkeqi  16078  bj-nnan  16100  bj-indind  16295  bj-omtrans  16319  bj-inf2vnlem1  16333  sscoll2  16351  2omap  16359  pw1map  16361  pwtrufal  16363  sssneq  16368  pw1nct  16369  nninfsellemsuc  16378  nninfomnilem  16384  nnnninfex  16388  exmidsbthrlem  16390  qdencn  16395  trilpo  16411  trirec0  16412  apdiff  16416  iswomninnlem  16417  iswomni0  16419  redcwlpo  16423  redc0  16425  reap0  16426  cndcap  16427  dceqnconst  16428  dcapnconst  16429  neapmkv  16436  neap0mkv  16437