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  1492  exsimpl  1628  sbequ2  1780  sbcof2  1821  sbequilem  1849  sbequ8  1858  euan  2094  mooran1  2110  eupickbi  2120  2exeu  2130  dimatis  2155  rexim  2584  r19.26  2616  r19.40  2644  rspcime  2867  rr19.28v  2896  elrab3t  2911  eueq3dc  2930  mosubt  2933  reu6  2945  sbc2iegf  3052  sbcralt  3058  sbcrext  3059  rmob  3074  csbiebt  3115  ssab2  3258  difdif  3279  uneqin  3405  indifdir  3410  undif3ss  3415  rexm  3541  eqifdc  3588  ifandc  3591  ifnebibdc  3596  difsn  3751  opprc1  3822  unissel  3860  ssmin  3885  abssexg  4207  undifexmid  4218  pwntru  4224  exmidundif  4231  exmidundifim  4232  opelopabsb  4285  sess1  4362  ordelord  4406  onin  4411  suctr  4446  abnexg  4471  ordtriexmidlem  4543  ordtri2or2exmid  4595  ontri2orexmidim  4596  tfi  4606  peano1  4618  peano2  4619  nnpredcl  4647  0nelxp  4679  0nelelxp  4680  brab2a  4704  mosubopt  4716  posng  4723  opabssxp  4725  ideqg  4803  relssres  4970  trin2  5045  dminss  5068  iota4an  5223  iota2  5232  iotam  5234  fun11uni  5312  imadiflem  5321  funimaexg  5326  fneq12  5335  fvelrnb  5591  dffo4  5692  ffnfv  5702  ffvresb  5707  fmptco  5710  fcoconst  5715  fcof1  5812  isotr  5845  isopolem  5851  f1oiso  5855  acexmidlemcase  5899  ovprc1  5940  fnoprabg  6005  op1steq  6212  dmmpog  6242  1stconst  6254  f1o2ndf1  6261  brtpos2  6284  tpostpos  6297  tposf12  6302  smores  6325  tfrlemi1  6365  tfr1onlembfn  6377  tfri1dALT  6384  tfrcllembfn  6390  freceq1  6425  freceq2  6426  frectfr  6433  omv2  6498  omsuc  6505  nnsucelsuc  6524  nntri3  6530  nnaordi  6541  nnmordi  6549  nnm00  6563  ecexr  6572  ertr  6582  swoer  6595  erth  6613  ecelqsdm  6639  iinerm  6641  ecinxp  6644  erovlem  6661  pmresg  6710  resixp  6767  elixpsn  6769  mapsnf1o  6771  dom3  6810  mapdom1g  6883  ssenen  6887  phpelm  6902  finexdc  6938  exmidpweq  6945  nnwetri  6952  fiintim  6965  infidc  6972  ssfii  7012  fiss  7015  dcfi  7019  supubti  7037  supisoex  7047  ordiso2  7073  inl11  7103  omp1eomlem  7132  nnnninf  7164  nninfisol  7171  ctssexmid  7188  ismkvnex  7193  omniwomnimkv  7205  nninfwlpor  7212  nninfwlpoim  7216  en2eleq  7234  en2other2  7235  exmidfodomrlemr  7241  exmidfodomrlemrALT  7242  exmidaclem  7247  djuen  7250  djudoml  7258  netap  7293  2omotaplemst  7297  exmidapne  7299  cc1  7304  dmaddpqlem  7416  distrnqg  7426  ltanqi  7441  ltmnqi  7442  ltaddnq  7446  ltrnqg  7459  ltnnnq  7462  enq0sym  7471  addnq0mo  7486  mulnq0mo  7487  addnnnq0  7488  distrnq0  7498  prarloclemn  7538  prarloc  7542  ltdfpr  7545  genplt2i  7549  addnqprl  7568  addnqpru  7569  nqprl  7590  appdivnq  7602  1idprl  7629  1idpru  7630  ltexpri  7652  recexpr  7677  cauappcvgprlemdisj  7690  archrecpr  7703  addsrmo  7782  mulsrmo  7783  addsrpr  7784  mulsrpr  7785  0idsr  7806  1idsr  7807  archsr  7821  prsradd  7825  prsrlt  7826  caucvgsr  7841  map2psrprg  7844  elrealeu  7868  muladd11r  8154  negeu  8189  pncan  8204  pncan3  8206  negsub  8246  addid0  8371  posdif  8453  ltnegcon1  8461  subge0  8473  suble0  8474  lesub0  8477  reapval  8574  reapneg  8595  ap0gt0  8638  aprcl  8644  lt0ap0  8646  recextlem1  8649  recapb  8669  div0ap  8700  recrecap  8707  rec11ap  8708  recgt0  8848  mulgt1  8861  lerec2  8887  recp1lt1  8897  recreclt  8898  ledivp1  8901  negiso  8953  nnsub  8999  avglt1  9198  nnrecl  9215  nnnn0addcl  9247  elnn0nn  9259  nn0ge2m1nn  9277  zaddcl  9334  eluzadd  9598  infregelbex  9640  divfnzn  9663  qaddcl  9677  qreccl  9684  cnref1o  9692  ge0p1rp  9727  divlt1lt  9766  divle1le  9767  addlelt  9810  xrre3  9864  xltnegi  9877  xaddval  9887  xaddcom  9903  xnegdi  9910  xposdif  9924  ixxssixx  9944  iccshftr  10036  iccshftl  10038  iccdil  10040  icccntr  10042  zltaddlt1le  10049  elfz2  10057  peano2fzr  10079  fzdcel  10082  fzsplit2  10092  fzaddel  10101  fzrev2  10127  fzrev2i  10128  fzrev3  10129  elfz1b  10132  fseq1p1m1  10136  uzsubfz0  10171  fzosubel3  10238  eluzgtdifelfzo  10239  fzofzp1b  10270  elfzomelpfzo  10273  exfzdc  10282  fvinim0ffz  10283  exbtwnzlemshrink  10291  qbtwnz  10294  qbtwnxr  10300  ico0  10304  elicore  10309  xqltnle  10310  apbtwnz  10317  flqge  10325  flqlt  10326  flqltnz  10330  flqbi2  10334  flqaddz  10340  flqmulnn0  10342  intfracq  10363  flqdiv  10364  q0mod  10398  q1mod  10399  mulp1mod1  10408  q2txmodxeq0  10427  modfzo0difsn  10438  frec2uzuzd  10445  frec2uzltd  10446  frec2uzrand  10448  uzennn  10479  seq3split  10524  seq3caopr  10528  exp3vallem  10567  exp3val  10568  expnnval  10569  exp1  10572  expcl2lemap  10578  rpexpcl  10585  expnegzap  10600  mulexp  10605  mulexpzap  10606  leexp2r  10620  leexp1a  10621  sq11  10639  subsq  10673  binom2  10678  binom3  10684  zesq  10685  bernneq  10687  sq11ap  10734  zzlesq  10735  mulsubdivbinom2ap  10738  apexp1  10745  facwordi  10767  facubnd  10772  facavg  10773  bcval  10776  bcval5  10790  hashennn  10807  fihashf1rn  10815  fseq1hash  10828  hashdifsn  10846  hashdifpr  10847  hashxp  10853  fiubz  10856  fiubnn  10857  fnfz0hash  10859  ffzo0hash  10861  shftfvalg  10874  ovshftex  10875  shftdm  10878  shftfib  10879  shftval  10881  shftf  10886  crre  10913  cjexp  10949  cjreim2  10960  uzin2  11043  rexuz3  11046  resqrexlemgt0  11076  resqrex  11082  sqrtgt0  11090  sqrtsq  11100  sqrtmsq  11101  absrpclap  11117  absext  11119  absmul  11125  absid  11127  absexp  11135  nn0abscl  11141  abslt  11144  absle  11145  recvalap  11153  abstri  11160  caubnd2  11173  qdenre  11258  maxabsle  11260  maxabslemval  11264  maxcl  11266  rexanre  11276  min1inf  11287  minabs  11291  minclpr  11292  mul0inf  11296  mingeb  11297  xrmaxiflemcl  11300  xrnegiso  11317  climconst2  11346  climmpt  11355  climres  11358  climcaucn  11406  sumeq1  11410  summodclem2a  11436  isumz  11444  fisumss  11447  fsumzcl2  11460  sumsnf  11464  isumclim3  11478  fsum2dlemstep  11489  fisumcom2  11493  fsumconst  11509  cvgcmpub  11531  binom  11539  binom1p  11540  binom1dif  11542  bcxmas  11544  divcnv  11552  geo2lim  11571  geoisum  11572  geoisumr  11573  geoisum1  11574  mertenslemi1  11590  mertensabs  11592  prod1dc  11641  fprodconst  11675  fprodcom2fi  11681  efcllem  11714  efcj  11728  efadd  11730  efexp  11737  efgt1p2  11750  tanvalap  11763  tanval2ap  11768  tanval3ap  11769  sinadd  11791  cosadd  11792  dvdsdc  11852  iddvdsexp  11869  dvdsadd  11890  dvds1  11906  odd2np1  11925  oddm1even  11927  m1exp1  11953  divalglemnn  11970  fldivndvdslt  11987  flodddiv4lt  11988  zsupcllemex  11994  infssuzcldc  11999  dvdsbnd  12004  gcdnncl  12015  zeqzmulgcd  12018  gcdneg  12030  modgcd  12039  bezoutlemex  12049  bezoutlemeu  12055  dfgcd3  12058  gcdzeq  12070  dvdssq  12079  algrf  12094  eucalgval2  12102  eucalgcvga  12107  lcmval  12112  gcddvdslcm  12122  lcmneg  12123  coprmgcdb  12137  qredeu  12146  divgcdcoprm0  12150  divgcdcoprmex  12151  cncongr1  12152  cncongr2  12153  cncongrcoprm  12155  prmind2  12169  dvdsnprmd  12174  exprmfct  12187  isprm6  12196  pw2dvdslemn  12214  oddpwdclemdc  12222  sqrt2irraplemnn  12228  divnumden  12245  divdenle  12246  nn0sqrtelqelz  12255  phivalfi  12261  crth  12273  eulerth  12282  prmdivdiv  12286  reumodprminv  12302  nnnn0modprm0  12304  nnoddn2prmb  12311  pcval  12345  pcidlem  12372  pcid  12373  pcneg  12374  pc2dvds  12379  pcz  12381  pcprod  12395  prmpwdvds  12404  4sqexercise1  12447  xpct  12464  znnen  12466  ennnfonelemg  12471  ennnfone  12493  ctinfom  12496  ctinf  12498  ssomct  12513  isstruct2im  12539  isstruct2r  12540  setsvalg  12559  setsslnid  12581  ressvalsets  12593  ressex  12594  2strbasg  12648  2stropg  12649  2strbas1g  12651  ressmulrg  12673  ressscag  12711  ressvscag  12712  ressipg  12713  restval  12767  restid2  12770  prdsex  12791  qusex  12819  fnpr2o  12833  xpsfval  12842  xpsval  12846  intopsn  12861  mgmidmo  12866  lidrididd  12876  ismnddef  12909  mndinvmod  12936  ismhm  12943  mhmex  12944  insubm  12967  dfgrp2  13002  grpsubval  13021  grpinvinv  13042  grpsubrcan  13056  grpsubadd  13063  grpaddsubass  13065  grpsubsub4  13068  grppnpcan2  13069  grpnpncan  13070  grpnpncan0  13071  grpnnncan2  13072  dfgrp3m  13074  dfgrp3me  13075  imasgrp2  13083  mhmmnd  13089  mulgfvalg  13094  mulgval  13095  mulgfng  13097  mulg1  13102  mulgnnp1  13103  mulgnndir  13124  mulgass  13132  mulgmodid  13134  issubg2m  13161  grpissubg  13166  isnsg  13174  isnsg3  13179  0nsg  13186  eqgfval  13194  eqger  13196  eqgen  13199  eqgcpbl  13200  quseccl  13205  isghm  13215  kerf1ghm  13246  conjghm  13248  conjsubg  13249  abladdsub  13287  ablpncan3  13289  ablsubsub23  13297  invghm  13301  subgabl  13304  mgpress  13320  rngdi  13329  rnglz  13334  imasrng  13345  srgmulgass  13378  srgrmhm  13383  isring  13389  ringo2times  13417  ringrng  13425  ringlz  13432  imasring  13451  opprrng  13464  opprrngbg  13465  opprring  13466  mulgass3  13472  dvdsrd  13481  dvdsrneg  13490  unitnegcl  13517  dvrvald  13521  dvrid  13524  dvr1  13525  dvrass  13526  dvrdir  13530  ringinvdv  13532  rhmex  13544  isrim0  13548  rhmval  13560  rhmdvdsr  13562  rhmopp  13563  elrhmunit  13564  rhmunitinv  13565  ringelnzr  13571  issubrng2  13594  issubrg2  13625  aprap  13645  lmodvs1  13675  lmod0vs  13680  lmodvs0  13681  lmodvsmmulgdi  13682  lmodfopne  13685  lmodvneg1  13689  lss1  13721  islss3  13738  lsslss  13740  lss1d  13742  lspf  13748  lspsn  13775  lspsnneg  13779  sraval  13796  sraring  13808  qus1  13885  qusrhm  13887  dvdsrzring  13948  mulgghm2  13952  mulgrhm  13953  znval  13980  znf1o  13995  psrplusgg  14015  eltg2b  14075  difopn  14129  ntrcls0  14152  neii1  14168  restbasg  14189  resttopon  14192  restuni2  14198  cnrest2r  14258  tx1cn  14290  txcnp  14292  txcn  14296  txswaphmeo  14342  psmettri  14351  xmeteq0  14380  xmettri  14393  metrtri  14398  ssblex  14452  xmeter  14457  isxms2  14473  cnbl0  14555  cnblcld  14556  reopnap  14559  tgioo  14567  addcncntoplem  14572  rescncf  14589  cncfcdm  14590  mulc1cncf  14597  cncfcncntop  14601  addccncf  14607  cdivcncfap  14611  negcncf  14612  cnopnap  14618  suplociccex  14632  hoverlt1  14656  hovergt0  14657  dich0  14659  limccl  14666  ellimc3apf  14667  cnplimcim  14674  limccnp2lem  14683  reldvg  14686  dvbsssg  14693  dvcjbr  14710  dvcj  14711  dvfre  14712  dvrecap  14715  dvef  14726  reeff1olem  14730  pilem3  14742  ptolemy  14783  rplogcl  14838  rpcxpef  14853  cxprec  14869  rpcxproot  14872  rplogb1  14904  logbgt0b  14922  logbgcd1irr  14923  binom4  14935  wilthlem1  14936  lgslem4  14943  lgsval  14944  lgsval2lem  14950  lgsval4a  14962  lgsdir2lem3  14970  lgsdir2  14973  lgsne0  14978  lgsprme0  14982  lgsmulsqcoprm  14986  bj-nnan  15027  bj-indind  15223  bj-omtrans  15247  bj-inf2vnlem1  15261  sscoll2  15279  pwtrufal  15287  sssneq  15291  pw1nct  15292  nninfsellemsuc  15301  nninfomnilem  15307  exmidsbthrlem  15311  qdencn  15316  trilpo  15332  trirec0  15333  apdiff  15337  iswomninnlem  15338  iswomni0  15340  redcwlpo  15344  redc0  15346  reap0  15347  cndcap  15348  dceqnconst  15349  dcapnconst  15350  neapmkv  15357  neap0mkv  15358