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  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  3624  eqifdc  3674  ifandc  3678  ifnebibdc  3683  difsn  3847  opprc1  3921  unissel  3959  ssmin  3984  abssexg  4314  undifexmid  4325  pwntru  4331  exmidundif  4338  exmidundifim  4339  opelopabsb  4397  elopabran  4421  sess1  4477  ordelord  4521  onin  4526  suctr  4561  abnexg  4587  ifexg  4626  ordtriexmidlem  4661  ordtri2or2exmid  4713  ontri2orexmidim  4714  tfi  4724  peano1  4736  peano2  4737  nnpredcl  4765  0nelxp  4797  0nelelxp  4798  brab2a  4823  mosubopt  4835  posng  4842  opabssxp  4844  ideqg  4926  relssres  5096  trin2  5174  dminss  5197  iota4an  5353  iota2  5362  iotam  5364  fununfun  5419  fun11uni  5446  imadiflem  5455  funimaexg  5460  fneq12  5469  fvelrnb  5744  dffo4  5847  ffnfv  5857  ffvresb  5862  fmptco  5865  fcoconst  5870  funopsn  5882  fndmexb  5929  fcof1  5979  isotr  6012  isopolem  6018  f1oiso  6022  acexmidlemcase  6070  ovprc1  6112  fnoprabg  6179  elovmporab  6279  elovmporab1w  6280  uchoice  6361  op1steq  6403  dmmpog  6435  1stconst  6447  f1o2ndf1  6454  suppfnss  6487  suppssfvg  6493  brtpos2  6512  tpostpos  6525  tposf12  6530  smores  6553  tfrlemi1  6593  tfr1onlembfn  6605  tfri1dALT  6612  tfrcllembfn  6618  freceq1  6653  freceq2  6654  frectfr  6661  omv2  6728  omsuc  6735  nnsucelsuc  6754  nntri3  6760  nnaordi  6771  nnmordi  6779  nnm00  6793  ecexr  6802  ertr  6812  swoer  6825  erth  6843  ecelqsdm  6869  iinerm  6871  ecinxp  6874  erovlem  6891  pmresg  6947  resixp  7005  elixpsn  7007  mapsnf1o  7009  dom3  7052  modom  7098  mapdom1g  7137  ssenen  7142  phpelm  7158  finexdc  7197  exmidpweq  7206  nnwetri  7213  fiintim  7228  infidc  7238  suppeqfsuppbi  7285  ssfii  7298  fiss  7301  dcfi  7305  2omap  7308  supubti  7329  supisoex  7339  ordiso2  7365  inl11  7395  omp1eomlem  7424  nnnninf  7456  nninfisol  7463  ctssexmid  7480  ismkvnex  7485  omniwomnimkv  7497  nninfwlpor  7504  nninfwlpoim  7509  nninfinfwlpo  7510  en2eleq  7537  en2other2  7538  exmidfodomrlemr  7544  exmidfodomrlemrALT  7545  acnrcl  7547  exmidaclem  7554  djuen  7557  djudoml  7565  netap  7610  2omotaplemst  7614  exmidapne  7616  cc1  7621  acnccim  7628  dmaddpqlem  7734  distrnqg  7744  ltanqi  7759  ltmnqi  7760  ltaddnq  7764  ltrnqg  7777  ltnnnq  7780  enq0sym  7789  addnq0mo  7804  mulnq0mo  7805  addnnnq0  7806  distrnq0  7816  prarloclemn  7856  prarloc  7860  ltdfpr  7863  genplt2i  7867  addnqprl  7886  addnqpru  7887  nqprl  7908  appdivnq  7920  1idprl  7947  1idpru  7948  ltexpri  7970  recexpr  7995  cauappcvgprlemdisj  8008  archrecpr  8021  addsrmo  8100  mulsrmo  8101  addsrpr  8102  mulsrpr  8103  0idsr  8124  1idsr  8125  archsr  8139  prsradd  8143  prsrlt  8144  caucvgsr  8159  map2psrprg  8162  elrealeu  8186  muladd11r  8472  negeu  8507  pncan  8522  pncan3  8524  negsub  8564  addid0  8689  addeq0  8693  posdif  8773  ltnegcon1  8781  subge0  8793  suble0  8794  lesub0  8797  reapval  8894  reapneg  8915  ap0gt0  8958  aprcl  8964  lt0ap0  8966  recextlem1  8969  recapb  8991  div0ap  9022  recrecap  9029  rec11ap  9030  recgt0  9170  mulgt1  9183  lerec2  9209  recp1lt1  9219  recreclt  9220  ledivp1  9223  negiso  9275  nnsub  9322  avglt1  9523  nnrecl  9540  nnnn0addcl  9572  elnn0nn  9584  fcdmnn0fsuppg  9597  nn0ge2m1nn  9606  zaddcl  9663  eluzmn  9907  eluzadd  9930  infregelbex  9977  divfnzn  10000  qaddcl  10014  qreccl  10021  cnref1o  10030  ge0p1rp  10065  divlt1lt  10104  divle1le  10105  addlelt  10148  xrre3  10203  xltnegi  10216  xaddval  10226  xaddcom  10242  xnegdi  10249  xposdif  10263  ixxssixx  10283  iccshftr  10375  iccshftl  10377  iccdil  10379  icccntr  10381  zltaddlt1le  10389  elfz2  10397  peano2fzr  10420  fzdcel  10423  fzsplit2  10433  fzaddel  10443  fzrev2  10470  fzrev2i  10471  fzrev3  10472  elfz1b  10475  fseq1p1m1  10479  uzsubfz0  10514  fzosubel3  10592  eluzgtdifelfzo  10593  fzofzp1b  10624  elfzomelpfzo  10627  exfzdc  10637  fvinim0ffz  10638  zsupcllemex  10641  infssuzcldc  10646  exbtwnzlemshrink  10661  qbtwnz  10664  qbtwnxr  10670  ico0  10674  elicore  10679  xqltnle  10680  apbtwnz  10687  flqge  10695  flqlt  10696  flqltnz  10700  flqbi2  10704  flqaddz  10710  flqmulnn0  10712  intfracq  10735  flqdiv  10736  q0mod  10770  q1mod  10771  mulp1mod1  10780  q2txmodxeq0  10799  modfzo0difsn  10810  frec2uzuzd  10817  frec2uzltd  10818  frec2uzrand  10820  uzennn  10851  seqfveq2g  10892  seq3split  10903  seqsplitg  10904  seq3caopr  10910  seqcaoprg  10911  seqf1oglem2  10935  seqf1og  10936  exp3vallem  10955  exp3val  10956  expnnval  10957  exp1  10960  expcl2lemap  10966  rpexpcl  10973  expnegzap  10988  mulexp  10993  mulexpzap  10994  leexp2r  11008  leexp1a  11009  sq11  11027  subsq  11061  binom2  11066  binom3  11072  zesq  11074  bernneq  11076  sq11ap  11123  zzlesq  11124  mulsubdivbinom2ap  11127  apexp1  11134  facwordi  11156  facubnd  11161  facavg  11162  bcval  11165  bcval5  11179  hashennn  11197  fihashf1rn  11205  fseq1hash  11219  hashdifsn  11238  hashdifpr  11239  hashxp  11245  hashmap  11246  fiubz  11250  fiubnn  11251  fnfz0hash  11253  ffzo0hash  11255  ssenneg  11258  hashfibclem  11260  hashf1  11265  hash2en  11273  wrdval  11285  ffz0iswrdnn0  11309  wrdsymb0  11315  ccatsymb  11348  ccatval21sw  11351  lswccatn0lsw  11357  ccatalpha  11359  ccatrcl1  11360  s111  11377  ccat1st1st  11387  lswccats1fst  11390  swrdlen2  11412  swrdfv2  11413  swrdsbslen  11416  swrds1  11418  ccatswrd  11420  pfxval  11424  pfxclg  11428  pfxmpt  11430  pfxid  11436  pfxfv0  11442  pfxtrcfv0  11444  pfxfvlsw  11445  pfxeq  11446  ccatpfx  11451  swrdpfx  11457  lenrevpfxcctswrd  11462  wrdeqs1cat  11470  cats1un  11471  swrdccatin1  11475  pfxccatin12lem2a  11477  pfxccatin12lem1  11478  pfxccatin12lem3  11482  pfxccatin12  11483  swrdccat  11485  pfxccat3a  11488  swrdccat3blem  11489  swrdccat3b  11490  reuccatpfxs1lem  11496  reuccatpfxs1  11497  s2cl  11535  s2fv0g  11537  shftfvalg  11561  ovshftex  11562  shftdm  11565  shftfib  11566  shftval  11568  shftf  11573  crre  11600  cjexp  11636  cjreim2  11648  uzin2  11731  rexuz3  11734  resqrexlemgt0  11764  resqrex  11770  sqrtgt0  11778  sqrtsq  11788  sqrtmsq  11789  absrpclap  11805  absext  11807  absmul  11813  absid  11815  absexp  11823  nn0abscl  11829  abslt  11832  absle  11833  recvalap  11841  abstri  11848  caubnd2  11861  qdenre  11946  maxabsle  11948  maxabslemval  11952  maxcl  11954  rexanre  11964  min1inf  11976  minabs  11980  minclpr  11981  mul0inf  11985  mingeb  11986  xrmaxiflemcl  11989  xrnegiso  12006  climconst2  12035  climmpt  12044  climres  12047  climcaucn  12095  sumeq1  12099  summodclem2a  12126  isumz  12134  fisumss  12137  fsumzcl2  12150  sumsnf  12154  isumclim3  12168  fsum2dlemstep  12179  fisumcom2  12183  fsumconst  12199  cvgcmpub  12221  binom  12229  binom1p  12230  binom1dif  12232  bcxmas  12234  divcnv  12242  geo2lim  12261  geoisum  12262  geoisumr  12263  geoisum1  12264  mertenslemi1  12280  mertensabs  12282  prod1dc  12331  fprodconst  12365  fprodcom2fi  12371  efcllem  12404  efcj  12418  efadd  12420  efexp  12427  efgt1p2  12440  tanvalap  12453  tanval2ap  12458  tanval3ap  12459  sinadd  12481  cosadd  12482  dvdsdc  12543  iddvdsexp  12560  dvdsadd  12581  dvds1  12598  odd2np1  12618  oddm1even  12620  m1exp1  12646  divalglemnn  12663  fldivndvdslt  12682  flodddiv4lt  12683  bitsp1  12696  bitsmod  12701  bitsfi  12702  bitscmp  12703  bitsinv1lem  12706  dvdsbnd  12711  gcdnncl  12722  zeqzmulgcd  12725  gcdneg  12737  modgcd  12746  bezoutlemex  12756  bezoutlemeu  12762  dfgcd3  12765  gcdzeq  12777  dvdssq  12786  algrf  12801  eucalgval2  12809  eucalgcvga  12814  lcmval  12819  gcddvdslcm  12829  lcmneg  12830  coprmgcdb  12844  qredeu  12853  divgcdcoprm0  12857  divgcdcoprmex  12858  cncongr1  12859  cncongr2  12860  cncongrcoprm  12862  prmind2  12876  dvdsnprmd  12881  exprmfct  12894  isprm6  12903  pw2dvdslemn  12921  oddpwdclemdc  12929  sqrt2irraplemnn  12935  divnumden  12952  divdenle  12953  nn0sqrtelqelz  12962  phivalfi  12968  crth  12980  eulerth  12989  prmdivdiv  12993  reumodprminv  13010  nnnn0modprm0  13012  nnoddn2prmb  13019  pcval  13053  pcidlem  13080  pcid  13081  pcneg  13082  pc2dvds  13087  pcz  13089  pcprod  13103  prmpwdvds  13112  4sqexercise1  13155  2expltfac  13196  ballotfilemfval  13207  ballotfilemefi  13215  ballotfilemodife  13218  ballotfilem4  13219  ballotfilemsval  13230  ballotfilemieq  13238  ballotfilemrv  13241  ballotfilemrinv0  13254  xpct  13265  znnen  13267  ennnfonelemg  13272  ennnfone  13294  ctinfom  13297  ctinf  13299  ssomct  13314  isstruct2im  13340  isstruct2r  13341  setsvalg  13360  setsslnid  13382  ressvalsets  13395  ressex  13396  2strbasg  13451  2stropg  13452  2strbas1g  13454  ressmulrg  13476  ressscag  13514  ressvscag  13515  ressipg  13516  restval  13576  restid2  13579  qusex  13623  fnpr2o  13637  xpsfval  13646  intopsn  13664  mgmidmo  13669  lidrididd  13679  ismnddef  13708  mndinvmod  13735  imasmnd2  13736  ismhm  13745  mhmex  13746  insubm  13769  dfgrp2  13809  grpsubval  13828  grpinvinv  13849  grpsubrcan  13863  grpsubadd  13870  grpaddsubass  13872  grpsubsub4  13875  grppnpcan2  13876  grpnpncan  13877  grpnpncan0  13878  grpnnncan2  13879  dfgrp3m  13881  dfgrp3me  13882  imasgrp2  13890  mhmmnd  13896  mulgfvalg  13901  mulgval  13902  mulgfng  13904  mulg1  13909  mulgnnp1  13910  mulgnndir  13931  mulgass  13939  mulgmodid  13941  issubg2m  13969  grpissubg  13974  isnsg  13982  isnsg3  13987  0nsg  13994  eqgfval  14002  eqger  14004  eqgen  14007  eqgcpbl  14008  quseccl  14013  isghm  14023  kerf1ghm  14054  conjghm  14056  conjsubg  14057  abladdsub  14096  ablpncan3  14098  ablsubsub23  14106  invghm  14110  subgabl  14113  prdsex  14149  xpsval  14178  pwsval  14181  mgpress  14205  rngdi  14214  rnglz  14219  imasrng  14230  srgmulgass  14267  srgrmhm  14272  isring  14278  ringo2times  14306  ringrng  14314  ringlz  14321  imasring  14342  opprrng  14355  opprrngbg  14356  opprring  14357  mulgass3  14364  dvdsrd  14374  dvdsrneg  14383  unitnegcl  14410  dvrvald  14414  dvrid  14417  dvr1  14418  dvrass  14419  dvrdir  14423  ringinvdv  14425  rhmex  14437  isrim0  14441  rhmval  14453  rhmdvdsr  14455  rhmopp  14456  elrhmunit  14457  rhmunitinv  14458  isnzr2  14464  ringelnzr  14467  issubrng2  14491  issubrg2  14522  ringunitap  14566  aprap  14571  aprnzr  14572  opprdrng  14593  lmodvs1  14625  lmod0vs  14630  lmodvs0  14631  lmodvsmmulgdi  14632  lmodfopne  14635  lmodvneg1  14639  lss1  14671  islss3  14688  lsslss  14690  lss1d  14692  lspf  14698  lspsn  14725  lspsnneg  14729  sraval  14746  sraring  14758  qus1  14835  qusrhm  14837  cnfldui  14896  dvdsrzring  14910  mulgghm2  14915  mulgrhm  14916  znval  14943  znf1o  14958  psrbagfi  14982  psrbagconcl  14986  psrplusgg  14992  mplgrpfi  15020  eltg2b  15078  difopn  15132  ntrcls0  15155  neii1  15171  restbasg  15192  resttopon  15195  restuni2  15201  cnrest2r  15261  tx1cn  15293  txcnp  15295  txcn  15299  txswaphmeo  15345  psmettri  15354  xmeteq0  15383  xmettri  15396  metrtri  15401  ssblex  15455  xmeter  15460  isxms2  15476  cnbl0  15558  cnblcld  15559  reopnap  15570  tgioo  15578  addcncntoplem  15585  expcn  15593  rescncf  15605  cncfcdm  15606  mulc1cncf  15613  cncfcncntop  15617  addccncf  15624  cdivcncfap  15628  negcncf  15629  cnopnap  15635  suplociccex  15649  hoverlt1  15673  hovergt0  15674  dich0  15676  limccl  15683  ellimc3apf  15684  cnplimcim  15691  limccnp2lem  15700  reldvg  15703  dvbsssg  15710  dvcjbr  15732  dvcj  15733  dvfre  15734  dvrecap  15737  dvef  15751  plyaddcl  15778  plymulcl  15779  plysubcl  15780  plyrecj  15787  reeff1olem  15795  pilem3  15807  ptolemy  15848  rplogcl  15903  rpcxpef  15919  cxprec  15935  rpcxproot  15939  rplogb1  15973  logbgt0b  15991  logbgcd1irr  15992  binom4  16004  wilthlem1  16008  sgmnncl  16016  dvdsppwf1o  16017  mersenne  16025  lgslem4  16036  lgsval  16037  lgsval2lem  16043  lgsval4a  16055  lgsdir2lem3  16063  lgsdir2  16066  lgsne0  16071  lgsprme0  16075  lgsmulsqcoprm  16079  gausslemma2dlem0a  16082  gausslemma2dlem1a  16091  2lgslem1b  16122  2lgslem2  16125  2lgsoddprm  16146  struct2slots2dom  16193  structvtxval  16194  structiedg0val  16195  struct2griedg  16201  edgstruct  16219  uhgr0vb  16239  incistruhgr  16245  umgrvad2edg  16366  uspgredg2vlem  16375  uspgredg2v  16376  usgredg2v  16379  ushgredgedg  16381  ushgredgedgloop  16383  usgr0vb  16388  uhgr0vusgr  16393  edg0usgr  16402  subupgr  16428  upgrspanop  16438  umgrspanop  16439  usgrspanop  16440  vtxdgfval  16443  wksfval  16477  wlkpropg  16479  uspgr2wlkeq2  16521  uspgr2wlkeqi  16522  upgr2wlkdc  16532  trlsex  16542  clwwlkccatlem  16555  clwwlkng  16560  clwwlkext2edg  16577  clwwlknccat  16578  umgr2cwwkdifex  16580  clwwlknonel  16587  clwwlknonccat  16588  clwwlknonex2lem2  16593  clwwlknun  16596  eupthsg  16600  eupth2lem3lem6fi  16626  dichmul0orlem7  16673  dichmul0or  16674  bj-nnan  16678  bj-indind  16872  bj-omtrans  16896  bj-inf2vnlem1  16910  sscoll2  16928  pw1map  16939  pwtrufal  16941  sssneq  16946  pw1nct  16947  exmidnotnotr  16949  nninfsellemsuc  16960  nninfomnilem  16966  nnnninfex  16970  exmidsbthrlem  16972  qdencn  16977  trilpo  16997  trirec0  16998  apdiff  17002  iswomninnlem  17004  iswomni0  17006  redcwlpo  17010  redc0  17012  reap0  17013  cndcap  17014  dceqnconst  17015  dcapnconst  17016  neapmkv  17023  neap0mkv  17024