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  2930  rr19.28v  2959  elrab3t  2974  eueq3dc  2993  mosubt  2996  reu6  3008  sbc2iegf  3115  sbcralt  3121  sbcrext  3122  rmob  3138  csbiebt  3180  ssab2  3324  difdif  3346  uneqin  3474  indifdir  3479  undif3ss  3484  rexm  3611  eqifdc  3661  ifandc  3665  ifnebibdc  3670  difsn  3833  opprc1  3907  unissel  3945  ssmin  3970  abssexg  4297  undifexmid  4308  pwntru  4314  exmidundif  4321  exmidundifim  4322  opelopabsb  4380  elopabran  4404  sess1  4460  ordelord  4504  onin  4509  suctr  4544  abnexg  4569  ifexg  4608  ordtriexmidlem  4643  ordtri2or2exmid  4695  ontri2orexmidim  4696  tfi  4706  peano1  4718  peano2  4719  nnpredcl  4747  0nelxp  4779  0nelelxp  4780  brab2a  4805  mosubopt  4817  posng  4824  opabssxp  4826  ideqg  4908  relssres  5078  trin2  5156  dminss  5179  iota4an  5335  iota2  5344  iotam  5346  fununfun  5401  fun11uni  5428  imadiflem  5437  funimaexg  5442  fneq12  5451  fvelrnb  5726  dffo4  5827  ffnfv  5837  ffvresb  5842  fmptco  5845  fcoconst  5850  funopsn  5862  fndmexb  5909  fcof1  5958  isotr  5991  isopolem  5997  f1oiso  6001  acexmidlemcase  6047  ovprc1  6089  fnoprabg  6156  elovmporab  6256  elovmporab1w  6257  uchoice  6333  op1steq  6375  dmmpog  6407  1stconst  6419  f1o2ndf1  6426  suppfnss  6459  suppssfvg  6465  brtpos2  6484  tpostpos  6497  tposf12  6502  smores  6525  tfrlemi1  6565  tfr1onlembfn  6577  tfri1dALT  6584  tfrcllembfn  6590  freceq1  6625  freceq2  6626  frectfr  6633  omv2  6700  omsuc  6707  nnsucelsuc  6726  nntri3  6732  nnaordi  6743  nnmordi  6751  nnm00  6765  ecexr  6774  ertr  6784  swoer  6797  erth  6815  ecelqsdm  6841  iinerm  6843  ecinxp  6846  erovlem  6863  pmresg  6912  resixp  6970  elixpsn  6972  mapsnf1o  6974  dom3  7017  modom  7063  mapdom1g  7102  ssenen  7107  phpelm  7123  finexdc  7162  exmidpweq  7171  nnwetri  7178  fiintim  7193  infidc  7203  suppeqfsuppbi  7250  ssfii  7263  fiss  7266  dcfi  7270  2omap  7271  supubti  7292  supisoex  7302  ordiso2  7328  inl11  7358  omp1eomlem  7387  nnnninf  7419  nninfisol  7426  ctssexmid  7443  ismkvnex  7448  omniwomnimkv  7460  nninfwlpor  7467  nninfwlpoim  7472  nninfinfwlpo  7473  en2eleq  7500  en2other2  7501  exmidfodomrlemr  7507  exmidfodomrlemrALT  7508  acnrcl  7510  exmidaclem  7517  djuen  7520  djudoml  7528  netap  7570  2omotaplemst  7574  exmidapne  7576  cc1  7581  acnccim  7588  dmaddpqlem  7694  distrnqg  7704  ltanqi  7719  ltmnqi  7720  ltaddnq  7724  ltrnqg  7737  ltnnnq  7740  enq0sym  7749  addnq0mo  7764  mulnq0mo  7765  addnnnq0  7766  distrnq0  7776  prarloclemn  7816  prarloc  7820  ltdfpr  7823  genplt2i  7827  addnqprl  7846  addnqpru  7847  nqprl  7868  appdivnq  7880  1idprl  7907  1idpru  7908  ltexpri  7930  recexpr  7955  cauappcvgprlemdisj  7968  archrecpr  7981  addsrmo  8060  mulsrmo  8061  addsrpr  8062  mulsrpr  8063  0idsr  8084  1idsr  8085  archsr  8099  prsradd  8103  prsrlt  8104  caucvgsr  8119  map2psrprg  8122  elrealeu  8146  muladd11r  8431  negeu  8466  pncan  8481  pncan3  8483  negsub  8523  addid0  8648  posdif  8731  ltnegcon1  8739  subge0  8751  suble0  8752  lesub0  8755  reapval  8852  reapneg  8873  ap0gt0  8916  aprcl  8922  lt0ap0  8924  recextlem1  8927  recapb  8947  div0ap  8978  recrecap  8985  rec11ap  8986  recgt0  9126  mulgt1  9139  lerec2  9165  recp1lt1  9175  recreclt  9176  ledivp1  9179  negiso  9231  nnsub  9278  avglt1  9479  nnrecl  9496  nnnn0addcl  9528  elnn0nn  9540  fcdmnn0fsuppg  9553  nn0ge2m1nn  9562  zaddcl  9619  eluzmn  9863  eluzadd  9886  infregelbex  9933  divfnzn  9956  qaddcl  9970  qreccl  9977  cnref1o  9986  ge0p1rp  10021  divlt1lt  10060  divle1le  10061  addlelt  10104  xrre3  10158  xltnegi  10171  xaddval  10181  xaddcom  10197  xnegdi  10204  xposdif  10218  ixxssixx  10238  iccshftr  10330  iccshftl  10332  iccdil  10334  icccntr  10336  zltaddlt1le  10344  elfz2  10352  peano2fzr  10374  fzdcel  10377  fzsplit2  10387  fzaddel  10396  fzrev2  10423  fzrev2i  10424  fzrev3  10425  elfz1b  10428  fseq1p1m1  10432  uzsubfz0  10467  fzosubel3  10545  eluzgtdifelfzo  10546  fzofzp1b  10577  elfzomelpfzo  10580  exfzdc  10590  fvinim0ffz  10591  zsupcllemex  10594  infssuzcldc  10599  exbtwnzlemshrink  10612  qbtwnz  10615  qbtwnxr  10621  ico0  10625  elicore  10630  xqltnle  10631  apbtwnz  10638  flqge  10646  flqlt  10647  flqltnz  10651  flqbi2  10655  flqaddz  10661  flqmulnn0  10663  intfracq  10686  flqdiv  10687  q0mod  10721  q1mod  10722  mulp1mod1  10731  q2txmodxeq0  10750  modfzo0difsn  10761  frec2uzuzd  10768  frec2uzltd  10769  frec2uzrand  10771  uzennn  10802  seqfveq2g  10843  seq3split  10854  seqsplitg  10855  seq3caopr  10861  seqcaoprg  10862  seqf1oglem2  10886  seqf1og  10887  exp3vallem  10906  exp3val  10907  expnnval  10908  exp1  10911  expcl2lemap  10917  rpexpcl  10924  expnegzap  10939  mulexp  10944  mulexpzap  10945  leexp2r  10959  leexp1a  10960  sq11  10978  subsq  11012  binom2  11017  binom3  11023  zesq  11024  bernneq  11026  sq11ap  11073  zzlesq  11074  mulsubdivbinom2ap  11077  apexp1  11084  facwordi  11106  facubnd  11111  facavg  11112  bcval  11115  bcval5  11129  hashennn  11147  fihashf1rn  11155  fseq1hash  11169  hashdifsn  11188  hashdifpr  11189  hashxp  11195  hashmap  11196  fiubz  11200  fiubnn  11201  fnfz0hash  11203  ffzo0hash  11205  ssenneg  11208  hashfibclem  11210  hash2en  11219  wrdval  11231  ffz0iswrdnn0  11255  wrdsymb0  11261  ccatsymb  11294  ccatval21sw  11297  lswccatn0lsw  11303  ccatalpha  11305  ccatrcl1  11306  s111  11323  ccat1st1st  11333  lswccats1fst  11336  swrdlen2  11358  swrdfv2  11359  swrdsbslen  11362  swrds1  11364  ccatswrd  11366  pfxval  11370  pfxclg  11374  pfxmpt  11376  pfxid  11382  pfxfv0  11388  pfxtrcfv0  11390  pfxfvlsw  11391  pfxeq  11392  ccatpfx  11397  swrdpfx  11403  lenrevpfxcctswrd  11408  wrdeqs1cat  11416  cats1un  11417  swrdccatin1  11421  pfxccatin12lem2a  11423  pfxccatin12lem1  11424  pfxccatin12lem3  11428  pfxccatin12  11429  swrdccat  11431  pfxccat3a  11434  swrdccat3blem  11435  swrdccat3b  11436  reuccatpfxs1lem  11442  reuccatpfxs1  11443  s2cl  11481  s2fv0g  11483  shftfvalg  11507  ovshftex  11508  shftdm  11511  shftfib  11512  shftval  11514  shftf  11519  crre  11546  cjexp  11582  cjreim2  11593  uzin2  11676  rexuz3  11679  resqrexlemgt0  11709  resqrex  11715  sqrtgt0  11723  sqrtsq  11733  sqrtmsq  11734  absrpclap  11750  absext  11752  absmul  11758  absid  11760  absexp  11768  nn0abscl  11774  abslt  11777  absle  11778  recvalap  11786  abstri  11793  caubnd2  11806  qdenre  11891  maxabsle  11893  maxabslemval  11897  maxcl  11899  rexanre  11909  min1inf  11921  minabs  11925  minclpr  11926  mul0inf  11930  mingeb  11931  xrmaxiflemcl  11934  xrnegiso  11951  climconst2  11980  climmpt  11989  climres  11992  climcaucn  12040  sumeq1  12044  summodclem2a  12071  isumz  12079  fisumss  12082  fsumzcl2  12095  sumsnf  12099  isumclim3  12113  fsum2dlemstep  12124  fisumcom2  12128  fsumconst  12144  cvgcmpub  12166  binom  12174  binom1p  12175  binom1dif  12177  bcxmas  12179  divcnv  12187  geo2lim  12206  geoisum  12207  geoisumr  12208  geoisum1  12209  mertenslemi1  12225  mertensabs  12227  prod1dc  12276  fprodconst  12310  fprodcom2fi  12316  efcllem  12349  efcj  12363  efadd  12365  efexp  12372  efgt1p2  12385  tanvalap  12398  tanval2ap  12403  tanval3ap  12404  sinadd  12426  cosadd  12427  dvdsdc  12488  iddvdsexp  12505  dvdsadd  12526  dvds1  12543  odd2np1  12563  oddm1even  12565  m1exp1  12591  divalglemnn  12608  fldivndvdslt  12627  flodddiv4lt  12628  bitsp1  12641  bitsmod  12646  bitsfi  12647  bitscmp  12648  bitsinv1lem  12651  dvdsbnd  12656  gcdnncl  12667  zeqzmulgcd  12670  gcdneg  12682  modgcd  12691  bezoutlemex  12701  bezoutlemeu  12707  dfgcd3  12710  gcdzeq  12722  dvdssq  12731  algrf  12746  eucalgval2  12754  eucalgcvga  12759  lcmval  12764  gcddvdslcm  12774  lcmneg  12775  coprmgcdb  12789  qredeu  12798  divgcdcoprm0  12802  divgcdcoprmex  12803  cncongr1  12804  cncongr2  12805  cncongrcoprm  12807  prmind2  12821  dvdsnprmd  12826  exprmfct  12839  isprm6  12848  pw2dvdslemn  12866  oddpwdclemdc  12874  sqrt2irraplemnn  12880  divnumden  12897  divdenle  12898  nn0sqrtelqelz  12907  phivalfi  12913  crth  12925  eulerth  12934  prmdivdiv  12938  reumodprminv  12955  nnnn0modprm0  12957  nnoddn2prmb  12964  pcval  12998  pcidlem  13025  pcid  13026  pcneg  13027  pc2dvds  13032  pcz  13034  pcprod  13048  prmpwdvds  13057  4sqexercise1  13100  2expltfac  13141  ballotfilemfval  13150  ballotfilemodife  13158  ballotfilem4  13159  xpct  13164  znnen  13166  ennnfonelemg  13171  ennnfone  13193  ctinfom  13196  ctinf  13198  ssomct  13213  isstruct2im  13239  isstruct2r  13240  setsvalg  13259  setsslnid  13281  ressvalsets  13294  ressex  13295  2strbasg  13350  2stropg  13351  2strbas1g  13353  ressmulrg  13375  ressscag  13413  ressvscag  13414  ressipg  13415  restval  13475  restid2  13478  prdsex  13499  pwsval  13521  qusex  13555  fnpr2o  13569  xpsfval  13578  xpsval  13582  intopsn  13597  mgmidmo  13602  lidrididd  13612  ismnddef  13648  mndinvmod  13675  imasmnd2  13682  ismhm  13691  mhmex  13692  insubm  13715  dfgrp2  13757  grpsubval  13776  grpinvinv  13797  grpsubrcan  13811  grpsubadd  13818  grpaddsubass  13820  grpsubsub4  13823  grppnpcan2  13824  grpnpncan  13825  grpnpncan0  13826  grpnnncan2  13827  dfgrp3m  13829  dfgrp3me  13830  imasgrp2  13844  mhmmnd  13850  mulgfvalg  13855  mulgval  13856  mulgfng  13858  mulg1  13863  mulgnnp1  13864  mulgnndir  13885  mulgass  13893  mulgmodid  13895  issubg2m  13923  grpissubg  13928  isnsg  13936  isnsg3  13941  0nsg  13948  eqgfval  13956  eqger  13958  eqgen  13961  eqgcpbl  13962  quseccl  13967  isghm  13977  kerf1ghm  14008  conjghm  14010  conjsubg  14011  abladdsub  14049  ablpncan3  14051  ablsubsub23  14059  invghm  14063  subgabl  14066  mgpress  14092  rngdi  14101  rnglz  14106  imasrng  14117  srgmulgass  14150  srgrmhm  14155  isring  14161  ringo2times  14189  ringrng  14197  ringlz  14204  imasring  14225  opprrng  14238  opprrngbg  14239  opprring  14240  mulgass3  14246  dvdsrd  14256  dvdsrneg  14265  unitnegcl  14292  dvrvald  14296  dvrid  14299  dvr1  14300  dvrass  14301  dvrdir  14305  ringinvdv  14307  rhmex  14319  isrim0  14323  rhmval  14335  rhmdvdsr  14337  rhmopp  14338  elrhmunit  14339  rhmunitinv  14340  isnzr2  14346  ringelnzr  14349  issubrng2  14372  issubrg2  14403  aprap  14449  aprnzr  14450  lmodvs1  14481  lmod0vs  14486  lmodvs0  14487  lmodvsmmulgdi  14488  lmodfopne  14491  lmodvneg1  14495  lss1  14527  islss3  14544  lsslss  14546  lss1d  14548  lspf  14554  lspsn  14581  lspsnneg  14585  sraval  14602  sraring  14614  qus1  14691  qusrhm  14693  cnfldui  14754  dvdsrzring  14768  mulgghm2  14773  mulgrhm  14774  znval  14801  znf1o  14816  psrbagfi  14840  psrbagconcl  14844  psrplusgg  14850  mplgrpfi  14878  eltg2b  14936  difopn  14990  ntrcls0  15013  neii1  15029  restbasg  15050  resttopon  15053  restuni2  15059  cnrest2r  15119  tx1cn  15151  txcnp  15153  txcn  15157  txswaphmeo  15203  psmettri  15212  xmeteq0  15241  xmettri  15254  metrtri  15259  ssblex  15313  xmeter  15318  isxms2  15334  cnbl0  15416  cnblcld  15417  reopnap  15428  tgioo  15436  addcncntoplem  15443  expcn  15451  rescncf  15463  cncfcdm  15464  mulc1cncf  15471  cncfcncntop  15475  addccncf  15482  cdivcncfap  15486  negcncf  15487  cnopnap  15493  suplociccex  15507  hoverlt1  15531  hovergt0  15532  dich0  15534  limccl  15541  ellimc3apf  15542  cnplimcim  15549  limccnp2lem  15558  reldvg  15561  dvbsssg  15568  dvcjbr  15590  dvcj  15591  dvfre  15592  dvrecap  15595  dvef  15609  plyaddcl  15636  plymulcl  15637  plysubcl  15638  plyrecj  15645  reeff1olem  15653  pilem3  15665  ptolemy  15706  rplogcl  15761  rpcxpef  15776  cxprec  15792  rpcxproot  15796  rplogb1  15830  logbgt0b  15848  logbgcd1irr  15849  binom4  15861  wilthlem1  15865  sgmnncl  15873  dvdsppwf1o  15874  mersenne  15882  lgslem4  15893  lgsval  15894  lgsval2lem  15900  lgsval4a  15912  lgsdir2lem3  15920  lgsdir2  15923  lgsne0  15928  lgsprme0  15932  lgsmulsqcoprm  15936  gausslemma2dlem0a  15939  gausslemma2dlem1a  15948  2lgslem1b  15979  2lgslem2  15982  2lgsoddprm  16003  struct2slots2dom  16050  structvtxval  16051  structiedg0val  16052  struct2griedg  16058  edgstruct  16076  uhgr0vb  16096  incistruhgr  16102  umgrvad2edg  16223  uspgredg2vlem  16232  uspgredg2v  16233  usgredg2v  16236  ushgredgedg  16238  ushgredgedgloop  16240  usgr0vb  16245  uhgr0vusgr  16250  edg0usgr  16259  subupgr  16285  upgrspanop  16295  umgrspanop  16296  usgrspanop  16297  vtxdgfval  16300  wksfval  16334  wlkpropg  16336  uspgr2wlkeq2  16378  uspgr2wlkeqi  16379  upgr2wlkdc  16389  trlsex  16399  clwwlkccatlem  16412  clwwlkng  16417  clwwlkext2edg  16434  clwwlknccat  16435  umgr2cwwkdifex  16437  clwwlknonel  16444  clwwlknonccat  16445  clwwlknonex2lem2  16450  clwwlknun  16453  eupthsg  16457  eupth2lem3lem6fi  16483  bj-nnan  16525  bj-indind  16719  bj-omtrans  16743  bj-inf2vnlem1  16757  sscoll2  16775  pw1map  16786  pwtrufal  16788  sssneq  16793  pw1nct  16794  exmidnotnotr  16796  nninfsellemsuc  16807  nninfomnilem  16813  nnnninfex  16817  exmidsbthrlem  16819  qdencn  16824  trilpo  16844  trirec0  16845  apdiff  16849  iswomninnlem  16851  iswomni0  16853  redcwlpo  16857  redc0  16859  reap0  16860  cndcap  16861  dceqnconst  16863  dcapnconst  16864  neapmkv  16871  neap0mkv  16872