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  603  pm4.38  605  pm5.21  696  ioran  753  pm3.14  754  pm4.44  780  ordi  817  pm4.39  823  animorl  824  animorlr  826  pm5.16  829  pm5.54dc  919  intnanr  931  intnanrd  933  dcan  935  dedlema  971  dedlemb  972  pm4.42r  973  prlem2  976  simp1l  1023  simp2l  1025  simp3l  1027  3anandis  1358  xordc1  1404  anxordi  1411  falantru  1414  19.26  1495  exsimpl  1631  sbequ2  1783  sbcof2  1824  sbequilem  1852  sbequ8  1861  euan  2101  mooran1  2117  eupickbi  2127  2exeu  2137  dimatis  2162  rexim  2591  r19.26  2623  r19.40  2651  rspcime  2875  rr19.28v  2904  elrab3t  2919  eueq3dc  2938  mosubt  2941  reu6  2953  sbc2iegf  3060  sbcralt  3066  sbcrext  3067  rmob  3082  csbiebt  3124  ssab2  3268  difdif  3289  uneqin  3415  indifdir  3420  undif3ss  3425  rexm  3551  eqifdc  3597  ifandc  3600  ifnebibdc  3605  difsn  3760  opprc1  3831  unissel  3869  ssmin  3894  abssexg  4216  undifexmid  4227  pwntru  4233  exmidundif  4240  exmidundifim  4241  opelopabsb  4295  sess1  4373  ordelord  4417  onin  4422  suctr  4457  abnexg  4482  ifexg  4521  ordtriexmidlem  4556  ordtri2or2exmid  4608  ontri2orexmidim  4609  tfi  4619  peano1  4631  peano2  4632  nnpredcl  4660  0nelxp  4692  0nelelxp  4693  brab2a  4717  mosubopt  4729  posng  4736  opabssxp  4738  ideqg  4818  relssres  4985  trin2  5062  dminss  5085  iota4an  5240  iota2  5249  iotam  5251  fun11uni  5329  imadiflem  5338  funimaexg  5343  fneq12  5352  fvelrnb  5611  dffo4  5713  ffnfv  5723  ffvresb  5728  fmptco  5731  fcoconst  5736  fcof1  5833  isotr  5866  isopolem  5872  f1oiso  5876  acexmidlemcase  5920  ovprc1  5962  fnoprabg  6027  elovmporab  6127  elovmporab1w  6128  uchoice  6204  op1steq  6246  dmmpog  6276  1stconst  6288  f1o2ndf1  6295  brtpos2  6318  tpostpos  6331  tposf12  6336  smores  6359  tfrlemi1  6399  tfr1onlembfn  6411  tfri1dALT  6418  tfrcllembfn  6424  freceq1  6459  freceq2  6460  frectfr  6467  omv2  6532  omsuc  6539  nnsucelsuc  6558  nntri3  6564  nnaordi  6575  nnmordi  6583  nnm00  6597  ecexr  6606  ertr  6616  swoer  6629  erth  6647  ecelqsdm  6673  iinerm  6675  ecinxp  6678  erovlem  6695  pmresg  6744  resixp  6801  elixpsn  6803  mapsnf1o  6805  dom3  6844  mapdom1g  6917  ssenen  6921  phpelm  6936  finexdc  6972  exmidpweq  6979  nnwetri  6986  fiintim  7001  infidc  7009  ssfii  7049  fiss  7052  dcfi  7056  supubti  7074  supisoex  7084  ordiso2  7110  inl11  7140  omp1eomlem  7169  nnnninf  7201  nninfisol  7208  ctssexmid  7225  ismkvnex  7230  omniwomnimkv  7242  nninfwlpor  7249  nninfwlpoim  7253  en2eleq  7274  en2other2  7275  exmidfodomrlemr  7281  exmidfodomrlemrALT  7282  acnrcl  7284  exmidaclem  7291  djuen  7294  djudoml  7302  netap  7337  2omotaplemst  7341  exmidapne  7343  cc1  7348  acnccim  7355  dmaddpqlem  7461  distrnqg  7471  ltanqi  7486  ltmnqi  7487  ltaddnq  7491  ltrnqg  7504  ltnnnq  7507  enq0sym  7516  addnq0mo  7531  mulnq0mo  7532  addnnnq0  7533  distrnq0  7543  prarloclemn  7583  prarloc  7587  ltdfpr  7590  genplt2i  7594  addnqprl  7613  addnqpru  7614  nqprl  7635  appdivnq  7647  1idprl  7674  1idpru  7675  ltexpri  7697  recexpr  7722  cauappcvgprlemdisj  7735  archrecpr  7748  addsrmo  7827  mulsrmo  7828  addsrpr  7829  mulsrpr  7830  0idsr  7851  1idsr  7852  archsr  7866  prsradd  7870  prsrlt  7871  caucvgsr  7886  map2psrprg  7889  elrealeu  7913  muladd11r  8199  negeu  8234  pncan  8249  pncan3  8251  negsub  8291  addid0  8416  posdif  8499  ltnegcon1  8507  subge0  8519  suble0  8520  lesub0  8523  reapval  8620  reapneg  8641  ap0gt0  8684  aprcl  8690  lt0ap0  8692  recextlem1  8695  recapb  8715  div0ap  8746  recrecap  8753  rec11ap  8754  recgt0  8894  mulgt1  8907  lerec2  8933  recp1lt1  8943  recreclt  8944  ledivp1  8947  negiso  8999  nnsub  9046  avglt1  9247  nnrecl  9264  nnnn0addcl  9296  elnn0nn  9308  nn0ge2m1nn  9326  zaddcl  9383  eluzadd  9647  infregelbex  9689  divfnzn  9712  qaddcl  9726  qreccl  9733  cnref1o  9742  ge0p1rp  9777  divlt1lt  9816  divle1le  9817  addlelt  9860  xrre3  9914  xltnegi  9927  xaddval  9937  xaddcom  9953  xnegdi  9960  xposdif  9974  ixxssixx  9994  iccshftr  10086  iccshftl  10088  iccdil  10090  icccntr  10092  zltaddlt1le  10099  elfz2  10107  peano2fzr  10129  fzdcel  10132  fzsplit2  10142  fzaddel  10151  fzrev2  10177  fzrev2i  10178  fzrev3  10179  elfz1b  10182  fseq1p1m1  10186  uzsubfz0  10221  fzosubel3  10289  eluzgtdifelfzo  10290  fzofzp1b  10321  elfzomelpfzo  10324  exfzdc  10333  fvinim0ffz  10334  zsupcllemex  10337  infssuzcldc  10342  exbtwnzlemshrink  10355  qbtwnz  10358  qbtwnxr  10364  ico0  10368  elicore  10373  xqltnle  10374  apbtwnz  10381  flqge  10389  flqlt  10390  flqltnz  10394  flqbi2  10398  flqaddz  10404  flqmulnn0  10406  intfracq  10429  flqdiv  10430  q0mod  10464  q1mod  10465  mulp1mod1  10474  q2txmodxeq0  10493  modfzo0difsn  10504  frec2uzuzd  10511  frec2uzltd  10512  frec2uzrand  10514  uzennn  10545  seqfveq2g  10586  seq3split  10597  seqsplitg  10598  seq3caopr  10604  seqcaoprg  10605  seqf1oglem2  10629  seqf1og  10630  exp3vallem  10649  exp3val  10650  expnnval  10651  exp1  10654  expcl2lemap  10660  rpexpcl  10667  expnegzap  10682  mulexp  10687  mulexpzap  10688  leexp2r  10702  leexp1a  10703  sq11  10721  subsq  10755  binom2  10760  binom3  10766  zesq  10767  bernneq  10769  sq11ap  10816  zzlesq  10817  mulsubdivbinom2ap  10820  apexp1  10827  facwordi  10849  facubnd  10854  facavg  10855  bcval  10858  bcval5  10872  hashennn  10889  fihashf1rn  10897  fseq1hash  10910  hashdifsn  10928  hashdifpr  10929  hashxp  10935  fiubz  10938  fiubnn  10939  fnfz0hash  10941  ffzo0hash  10943  wrdval  10955  wrdsymb0  10984  shftfvalg  11000  ovshftex  11001  shftdm  11004  shftfib  11005  shftval  11007  shftf  11012  crre  11039  cjexp  11075  cjreim2  11086  uzin2  11169  rexuz3  11172  resqrexlemgt0  11202  resqrex  11208  sqrtgt0  11216  sqrtsq  11226  sqrtmsq  11227  absrpclap  11243  absext  11245  absmul  11251  absid  11253  absexp  11261  nn0abscl  11267  abslt  11270  absle  11271  recvalap  11279  abstri  11286  caubnd2  11299  qdenre  11384  maxabsle  11386  maxabslemval  11390  maxcl  11392  rexanre  11402  min1inf  11414  minabs  11418  minclpr  11419  mul0inf  11423  mingeb  11424  xrmaxiflemcl  11427  xrnegiso  11444  climconst2  11473  climmpt  11482  climres  11485  climcaucn  11533  sumeq1  11537  summodclem2a  11563  isumz  11571  fisumss  11574  fsumzcl2  11587  sumsnf  11591  isumclim3  11605  fsum2dlemstep  11616  fisumcom2  11620  fsumconst  11636  cvgcmpub  11658  binom  11666  binom1p  11667  binom1dif  11669  bcxmas  11671  divcnv  11679  geo2lim  11698  geoisum  11699  geoisumr  11700  geoisum1  11701  mertenslemi1  11717  mertensabs  11719  prod1dc  11768  fprodconst  11802  fprodcom2fi  11808  efcllem  11841  efcj  11855  efadd  11857  efexp  11864  efgt1p2  11877  tanvalap  11890  tanval2ap  11895  tanval3ap  11896  sinadd  11918  cosadd  11919  dvdsdc  11980  iddvdsexp  11997  dvdsadd  12018  dvds1  12035  odd2np1  12055  oddm1even  12057  m1exp1  12083  divalglemnn  12100  fldivndvdslt  12119  flodddiv4lt  12120  bitsp1  12133  bitsmod  12138  bitsfi  12139  bitscmp  12140  bitsinv1lem  12143  dvdsbnd  12148  gcdnncl  12159  zeqzmulgcd  12162  gcdneg  12174  modgcd  12183  bezoutlemex  12193  bezoutlemeu  12199  dfgcd3  12202  gcdzeq  12214  dvdssq  12223  algrf  12238  eucalgval2  12246  eucalgcvga  12251  lcmval  12256  gcddvdslcm  12266  lcmneg  12267  coprmgcdb  12281  qredeu  12290  divgcdcoprm0  12294  divgcdcoprmex  12295  cncongr1  12296  cncongr2  12297  cncongrcoprm  12299  prmind2  12313  dvdsnprmd  12318  exprmfct  12331  isprm6  12340  pw2dvdslemn  12358  oddpwdclemdc  12366  sqrt2irraplemnn  12372  divnumden  12389  divdenle  12390  nn0sqrtelqelz  12399  phivalfi  12405  crth  12417  eulerth  12426  prmdivdiv  12430  reumodprminv  12447  nnnn0modprm0  12449  nnoddn2prmb  12456  pcval  12490  pcidlem  12517  pcid  12518  pcneg  12519  pc2dvds  12524  pcz  12526  pcprod  12540  prmpwdvds  12549  4sqexercise1  12592  2expltfac  12633  xpct  12638  znnen  12640  ennnfonelemg  12645  ennnfone  12667  ctinfom  12670  ctinf  12672  ssomct  12687  isstruct2im  12713  isstruct2r  12714  setsvalg  12733  setsslnid  12755  ressvalsets  12767  ressex  12768  2strbasg  12822  2stropg  12823  2strbas1g  12825  ressmulrg  12847  ressscag  12885  ressvscag  12886  ressipg  12887  restval  12947  restid2  12950  prdsex  12971  pwsval  12993  qusex  13027  fnpr2o  13041  xpsfval  13050  xpsval  13054  intopsn  13069  mgmidmo  13074  lidrididd  13084  ismnddef  13120  mndinvmod  13147  imasmnd2  13154  ismhm  13163  mhmex  13164  insubm  13187  dfgrp2  13229  grpsubval  13248  grpinvinv  13269  grpsubrcan  13283  grpsubadd  13290  grpaddsubass  13292  grpsubsub4  13295  grppnpcan2  13296  grpnpncan  13297  grpnpncan0  13298  grpnnncan2  13299  dfgrp3m  13301  dfgrp3me  13302  imasgrp2  13316  mhmmnd  13322  mulgfvalg  13327  mulgval  13328  mulgfng  13330  mulg1  13335  mulgnnp1  13336  mulgnndir  13357  mulgass  13365  mulgmodid  13367  issubg2m  13395  grpissubg  13400  isnsg  13408  isnsg3  13413  0nsg  13420  eqgfval  13428  eqger  13430  eqgen  13433  eqgcpbl  13434  quseccl  13439  isghm  13449  kerf1ghm  13480  conjghm  13482  conjsubg  13483  abladdsub  13521  ablpncan3  13523  ablsubsub23  13531  invghm  13535  subgabl  13538  mgpress  13563  rngdi  13572  rnglz  13577  imasrng  13588  srgmulgass  13621  srgrmhm  13626  isring  13632  ringo2times  13660  ringrng  13668  ringlz  13675  imasring  13696  opprrng  13709  opprrngbg  13710  opprring  13711  mulgass3  13717  dvdsrd  13726  dvdsrneg  13735  unitnegcl  13762  dvrvald  13766  dvrid  13769  dvr1  13770  dvrass  13771  dvrdir  13775  ringinvdv  13777  rhmex  13789  isrim0  13793  rhmval  13805  rhmdvdsr  13807  rhmopp  13808  elrhmunit  13809  rhmunitinv  13810  isnzr2  13816  ringelnzr  13819  issubrng2  13842  issubrg2  13873  aprap  13918  lmodvs1  13948  lmod0vs  13953  lmodvs0  13954  lmodvsmmulgdi  13955  lmodfopne  13958  lmodvneg1  13962  lss1  13994  islss3  14011  lsslss  14013  lss1d  14015  lspf  14021  lspsn  14048  lspsnneg  14052  sraval  14069  sraring  14081  qus1  14158  qusrhm  14160  cnfldui  14221  dvdsrzring  14235  mulgghm2  14240  mulgrhm  14241  znval  14268  znf1o  14283  psrplusgg  14306  eltg2b  14374  difopn  14428  ntrcls0  14451  neii1  14467  restbasg  14488  resttopon  14491  restuni2  14497  cnrest2r  14557  tx1cn  14589  txcnp  14591  txcn  14595  txswaphmeo  14641  psmettri  14650  xmeteq0  14679  xmettri  14692  metrtri  14697  ssblex  14751  xmeter  14756  isxms2  14772  cnbl0  14854  cnblcld  14855  reopnap  14866  tgioo  14874  addcncntoplem  14881  expcn  14889  rescncf  14901  cncfcdm  14902  mulc1cncf  14909  cncfcncntop  14913  addccncf  14920  cdivcncfap  14924  negcncf  14925  cnopnap  14931  suplociccex  14945  hoverlt1  14969  hovergt0  14970  dich0  14972  limccl  14979  ellimc3apf  14980  cnplimcim  14987  limccnp2lem  14996  reldvg  14999  dvbsssg  15006  dvcjbr  15028  dvcj  15029  dvfre  15030  dvrecap  15033  dvef  15047  plyaddcl  15074  plymulcl  15075  plysubcl  15076  plyrecj  15083  reeff1olem  15091  pilem3  15103  ptolemy  15144  rplogcl  15199  rpcxpef  15214  cxprec  15230  rpcxproot  15234  rplogb1  15268  logbgt0b  15286  logbgcd1irr  15287  binom4  15299  wilthlem1  15300  sgmnncl  15308  dvdsppwf1o  15309  mersenne  15317  lgslem4  15328  lgsval  15329  lgsval2lem  15335  lgsval4a  15347  lgsdir2lem3  15355  lgsdir2  15358  lgsne0  15363  lgsprme0  15367  lgsmulsqcoprm  15371  gausslemma2dlem0a  15374  gausslemma2dlem1a  15383  2lgslem1b  15414  2lgslem2  15417  2lgsoddprm  15438  bj-nnan  15466  bj-indind  15662  bj-omtrans  15686  bj-inf2vnlem1  15700  sscoll2  15718  2omap  15726  pwtrufal  15728  sssneq  15733  pw1nct  15734  nninfsellemsuc  15743  nninfomnilem  15749  exmidsbthrlem  15753  qdencn  15758  trilpo  15774  trirec0  15775  apdiff  15779  iswomninnlem  15780  iswomni0  15782  redcwlpo  15786  redc0  15788  reap0  15789  cndcap  15790  dceqnconst  15791  dcapnconst  15792  neapmkv  15799  neap0mkv  15800