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  695  ioran  752  pm3.14  753  pm4.44  779  ordi  816  pm4.39  822  animorl  823  animorlr  825  pm5.16  828  pm5.54dc  918  intnanr  930  intnanrd  932  dcan  933  dedlema  969  dedlemb  970  pm4.42r  971  prlem2  974  simp1l  1021  simp2l  1023  simp3l  1025  3anandis  1347  xordc1  1393  anxordi  1400  falantru  1403  19.26  1481  exsimpl  1617  sbequ2  1769  sbcof2  1810  sbequilem  1838  sbequ8  1847  euan  2082  mooran1  2098  eupickbi  2108  2exeu  2118  dimatis  2143  rexim  2571  r19.26  2603  r19.40  2631  rspcime  2849  rr19.28v  2878  elrab3t  2893  eueq3dc  2912  mosubt  2915  reu6  2927  sbc2iegf  3034  sbcralt  3040  sbcrext  3041  rmob  3056  csbiebt  3097  ssab2  3240  difdif  3261  uneqin  3387  indifdir  3392  undif3ss  3397  rexm  3523  eqifdc  3570  ifandc  3573  difsn  3730  opprc1  3801  unissel  3839  ssmin  3864  abssexg  4183  undifexmid  4194  pwntru  4200  exmidundif  4207  exmidundifim  4208  opelopabsb  4261  sess1  4338  ordelord  4382  onin  4387  suctr  4422  abnexg  4447  ordtriexmidlem  4519  ordtri2or2exmid  4571  ontri2orexmidim  4572  tfi  4582  peano1  4594  peano2  4595  nnpredcl  4623  0nelxp  4655  0nelelxp  4656  brab2a  4680  mosubopt  4692  posng  4699  opabssxp  4701  ideqg  4779  relssres  4946  trin2  5021  dminss  5044  iota4an  5198  iota2  5207  iotam  5209  fun11uni  5287  imadiflem  5296  funimaexg  5301  fneq12  5310  fvelrnb  5564  dffo4  5665  ffnfv  5675  ffvresb  5680  fmptco  5683  fcoconst  5688  fcof1  5784  isotr  5817  isopolem  5823  f1oiso  5827  acexmidlemcase  5870  ovprc1  5911  fnoprabg  5976  op1steq  6180  dmmpog  6210  1stconst  6222  f1o2ndf1  6229  brtpos2  6252  tpostpos  6265  tposf12  6270  smores  6293  tfrlemi1  6333  tfr1onlembfn  6345  tfri1dALT  6352  tfrcllembfn  6358  freceq1  6393  freceq2  6394  frectfr  6401  omv2  6466  omsuc  6473  nnsucelsuc  6492  nntri3  6498  nnaordi  6509  nnmordi  6517  nnm00  6531  ecexr  6540  ertr  6550  swoer  6563  erth  6579  ecelqsdm  6605  iinerm  6607  ecinxp  6610  erovlem  6627  pmresg  6676  resixp  6733  elixpsn  6735  mapsnf1o  6737  dom3  6776  mapdom1g  6847  ssenen  6851  phpelm  6866  finexdc  6902  exmidpweq  6909  nnwetri  6915  fiintim  6928  ssfii  6973  fiss  6976  dcfi  6980  supubti  6998  supisoex  7008  ordiso2  7034  inl11  7064  omp1eomlem  7093  nnnninf  7124  nninfisol  7131  ctssexmid  7148  ismkvnex  7153  omniwomnimkv  7165  nninfwlpor  7172  nninfwlpoim  7176  en2eleq  7194  en2other2  7195  exmidfodomrlemr  7201  exmidfodomrlemrALT  7202  exmidaclem  7207  djuen  7210  djudoml  7218  netap  7253  2omotaplemst  7257  exmidapne  7259  cc1  7264  dmaddpqlem  7376  distrnqg  7386  ltanqi  7401  ltmnqi  7402  ltaddnq  7406  ltrnqg  7419  ltnnnq  7422  enq0sym  7431  addnq0mo  7446  mulnq0mo  7447  addnnnq0  7448  distrnq0  7458  prarloclemn  7498  prarloc  7502  ltdfpr  7505  genplt2i  7509  addnqprl  7528  addnqpru  7529  nqprl  7550  appdivnq  7562  1idprl  7589  1idpru  7590  ltexpri  7612  recexpr  7637  cauappcvgprlemdisj  7650  archrecpr  7663  addsrmo  7742  mulsrmo  7743  addsrpr  7744  mulsrpr  7745  0idsr  7766  1idsr  7767  archsr  7781  prsradd  7785  prsrlt  7786  caucvgsr  7801  map2psrprg  7804  elrealeu  7828  muladd11r  8113  negeu  8148  pncan  8163  pncan3  8165  negsub  8205  addid0  8330  posdif  8412  ltnegcon1  8420  subge0  8432  suble0  8433  lesub0  8436  reapval  8533  reapneg  8554  ap0gt0  8597  aprcl  8603  lt0ap0  8605  recextlem1  8608  recapb  8628  div0ap  8659  recrecap  8666  rec11ap  8667  recgt0  8807  mulgt1  8820  lerec2  8846  recp1lt1  8856  recreclt  8857  ledivp1  8860  negiso  8912  nnsub  8958  avglt1  9157  nnrecl  9174  nnnn0addcl  9206  elnn0nn  9218  nn0ge2m1nn  9236  zaddcl  9293  eluzadd  9556  infregelbex  9598  divfnzn  9621  qaddcl  9635  qreccl  9642  cnref1o  9650  ge0p1rp  9685  divlt1lt  9724  divle1le  9725  addlelt  9768  xrre3  9822  xltnegi  9835  xaddval  9845  xaddcom  9861  xnegdi  9868  xposdif  9882  ixxssixx  9902  iccshftr  9994  iccshftl  9996  iccdil  9998  icccntr  10000  zltaddlt1le  10007  elfz2  10015  peano2fzr  10037  fzdcel  10040  fzsplit2  10050  fzaddel  10059  fzrev2  10085  fzrev2i  10086  fzrev3  10087  elfz1b  10090  fseq1p1m1  10094  uzsubfz0  10129  fzosubel3  10196  eluzgtdifelfzo  10197  fzofzp1b  10228  elfzomelpfzo  10231  exfzdc  10240  fvinim0ffz  10241  exbtwnzlemshrink  10249  qbtwnz  10252  qbtwnxr  10258  ico0  10262  elicore  10267  apbtwnz  10274  flqge  10282  flqlt  10283  flqltnz  10287  flqbi2  10291  flqaddz  10297  flqmulnn0  10299  intfracq  10320  flqdiv  10321  q0mod  10355  q1mod  10356  mulp1mod1  10365  q2txmodxeq0  10384  modfzo0difsn  10395  frec2uzuzd  10402  frec2uzltd  10403  frec2uzrand  10405  uzennn  10436  seq3split  10479  seq3caopr  10483  exp3vallem  10521  exp3val  10522  expnnval  10523  exp1  10526  expcl2lemap  10532  rpexpcl  10539  expnegzap  10554  mulexp  10559  mulexpzap  10560  leexp2r  10574  leexp1a  10575  sq11  10593  subsq  10627  binom2  10632  binom3  10638  zesq  10639  bernneq  10641  sq11ap  10688  mulsubdivbinom2ap  10691  apexp1  10698  facwordi  10720  facubnd  10725  facavg  10726  bcval  10729  bcval5  10743  hashennn  10760  fihashf1rn  10768  fseq1hash  10781  hashdifsn  10799  hashdifpr  10800  hashxp  10806  fiubz  10809  fiubnn  10810  fnfz0hash  10812  ffzo0hash  10814  shftfvalg  10827  ovshftex  10828  shftdm  10831  shftfib  10832  shftval  10834  shftf  10839  crre  10866  cjexp  10902  cjreim2  10913  uzin2  10996  rexuz3  10999  resqrexlemgt0  11029  resqrex  11035  sqrtgt0  11043  sqrtsq  11053  sqrtmsq  11054  absrpclap  11070  absext  11072  absmul  11078  absid  11080  absexp  11088  nn0abscl  11094  abslt  11097  absle  11098  recvalap  11106  abstri  11113  caubnd2  11126  qdenre  11211  maxabsle  11213  maxabslemval  11217  maxcl  11219  rexanre  11229  min1inf  11240  minabs  11244  minclpr  11245  mul0inf  11249  mingeb  11250  xrmaxiflemcl  11253  xrnegiso  11270  climconst2  11299  climmpt  11308  climres  11311  climcaucn  11359  sumeq1  11363  summodclem2a  11389  isumz  11397  fisumss  11400  fsumzcl2  11413  sumsnf  11417  isumclim3  11431  fsum2dlemstep  11442  fisumcom2  11446  fsumconst  11462  cvgcmpub  11484  binom  11492  binom1p  11493  binom1dif  11495  bcxmas  11497  divcnv  11505  geo2lim  11524  geoisum  11525  geoisumr  11526  geoisum1  11527  mertenslemi1  11543  mertensabs  11545  prod1dc  11594  fprodconst  11628  fprodcom2fi  11634  efcllem  11667  efcj  11681  efadd  11683  efexp  11690  efgt1p2  11703  tanvalap  11716  tanval2ap  11721  tanval3ap  11722  sinadd  11744  cosadd  11745  dvdsdc  11805  iddvdsexp  11822  dvdsadd  11843  dvds1  11859  odd2np1  11878  oddm1even  11880  m1exp1  11906  divalglemnn  11923  fldivndvdslt  11940  flodddiv4lt  11941  zsupcllemex  11947  infssuzcldc  11952  dvdsbnd  11957  gcdnncl  11968  zeqzmulgcd  11971  gcdneg  11983  modgcd  11992  bezoutlemex  12002  bezoutlemeu  12008  dfgcd3  12011  gcdzeq  12023  dvdssq  12032  algrf  12045  eucalgval2  12053  eucalgcvga  12058  lcmval  12063  gcddvdslcm  12073  lcmneg  12074  coprmgcdb  12088  qredeu  12097  divgcdcoprm0  12101  divgcdcoprmex  12102  cncongr1  12103  cncongr2  12104  cncongrcoprm  12106  prmind2  12120  dvdsnprmd  12125  exprmfct  12138  isprm6  12147  pw2dvdslemn  12165  oddpwdclemdc  12173  sqrt2irraplemnn  12179  divnumden  12196  divdenle  12197  nn0sqrtelqelz  12206  phivalfi  12212  crth  12224  eulerth  12233  prmdivdiv  12237  reumodprminv  12253  nnnn0modprm0  12255  nnoddn2prmb  12262  pcval  12296  pcidlem  12322  pcid  12323  pcneg  12324  pc2dvds  12329  pcz  12331  pcprod  12344  prmpwdvds  12353  xpct  12397  znnen  12399  ennnfonelemg  12404  ennnfone  12426  ctinfom  12429  ctinf  12431  ssomct  12446  isstruct2im  12472  isstruct2r  12473  setsvalg  12492  setsslnid  12514  ressvalsets  12524  ressex  12525  2strbasg  12578  2stropg  12579  2strbas1g  12581  ressmulrg  12603  restval  12694  restid2  12697  prdsex  12718  fnpr2o  12758  xpsfval  12767  xpsval  12771  intopsn  12786  mgmidmo  12791  lidrididd  12801  ismnddef  12819  mndinvmod  12846  ismhm  12853  insubm  12872  dfgrp2  12902  grpsubval  12919  grpinvinv  12937  grpsubrcan  12951  grpsubadd  12958  grpaddsubass  12960  grpsubsub4  12963  grppnpcan2  12964  grpnpncan  12965  grpnpncan0  12966  grpnnncan2  12967  dfgrp3m  12969  dfgrp3me  12970  mhmmnd  12980  mulgfvalg  12985  mulgval  12986  mulgfng  12987  mulg1  12990  mulgnnp1  12991  mulgnndir  13012  mulgass  13020  mulgmodid  13022  issubg2m  13049  grpissubg  13054  isnsg  13062  isnsg3  13067  0nsg  13074  eqgfval  13081  eqger  13083  eqgen  13086  eqgcpbl  13087  abladdsub  13118  ablpncan3  13120  ablsubsub23  13128  mgpress  13141  srgmulgass  13172  srgrmhm  13177  isring  13183  ringo2times  13211  ringlz  13222  opprring  13249  mulgass3  13254  dvdsrd  13263  dvdsrneg  13272  unitnegcl  13299  dvrvald  13303  dvrid  13306  dvr1  13307  dvrass  13308  dvrdir  13312  ringinvdv  13314  ringelnzr  13328  issubrg2  13362  aprap  13376  lmodvs1  13406  lmod0vs  13411  lmodvs0  13412  lmodvsmmulgdi  13413  lmodfopne  13416  lmodvneg1  13420  dvdsrzring  13496  eltg2b  13557  difopn  13611  ntrcls0  13634  neii1  13650  restbasg  13671  resttopon  13674  restuni2  13680  cnrest2r  13740  tx1cn  13772  txcnp  13774  txcn  13778  txswaphmeo  13824  psmettri  13833  xmeteq0  13862  xmettri  13875  metrtri  13880  ssblex  13934  xmeter  13939  isxms2  13955  cnbl0  14037  cnblcld  14038  reopnap  14041  tgioo  14049  addcncntoplem  14054  rescncf  14071  cncfcdm  14072  mulc1cncf  14079  cncfcncntop  14083  addccncf  14089  cdivcncfap  14090  negcncf  14091  cnopnap  14097  suplociccex  14106  limccl  14131  ellimc3apf  14132  cnplimcim  14139  limccnp2lem  14148  reldvg  14151  dvbsssg  14158  dvcjbr  14175  dvcj  14176  dvfre  14177  dvrecap  14180  dvef  14191  reeff1olem  14195  pilem3  14207  ptolemy  14248  rplogcl  14303  rpcxpef  14318  cxprec  14334  rpcxproot  14337  rplogb1  14369  logbgt0b  14387  logbgcd1irr  14388  binom4  14400  lgslem4  14407  lgsval  14408  lgsval2lem  14414  lgsval4a  14426  lgsdir2lem3  14434  lgsdir2  14437  lgsne0  14442  lgsprme0  14446  lgsmulsqcoprm  14450  bj-nnan  14491  bj-indind  14687  bj-omtrans  14711  bj-inf2vnlem1  14725  sscoll2  14743  pwtrufal  14750  sssneq  14754  pw1nct  14755  nninfsellemsuc  14764  nninfomnilem  14770  exmidsbthrlem  14773  qdencn  14778  trilpo  14794  trirec0  14795  apdiff  14799  iswomninnlem  14800  iswomni0  14802  redcwlpo  14806  redc0  14808  reap0  14809  dceqnconst  14810  dcapnconst  14811  neapmkv  14818  neap0mkv  14819