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  1817  sbcof2  1858  sbequilem  1886  sbequ8  1895  euan  2136  mooran1  2152  eupickbi  2162  2exeu  2172  dimatis  2197  rexim  2627  r19.26  2660  r19.40  2688  rspcime  2918  rr19.28v  2947  elrab3t  2962  eueq3dc  2981  mosubt  2984  reu6  2996  sbc2iegf  3103  sbcralt  3109  sbcrext  3110  rmob  3126  csbiebt  3168  ssab2  3312  difdif  3334  uneqin  3460  indifdir  3465  undif3ss  3470  rexm  3596  eqifdc  3646  ifandc  3650  ifnebibdc  3655  difsn  3815  opprc1  3889  unissel  3927  ssmin  3952  abssexg  4278  undifexmid  4289  pwntru  4295  exmidundif  4302  exmidundifim  4303  opelopabsb  4360  elopabran  4384  sess1  4440  ordelord  4484  onin  4489  suctr  4524  abnexg  4549  ifexg  4588  ordtriexmidlem  4623  ordtri2or2exmid  4675  ontri2orexmidim  4676  tfi  4686  peano1  4698  peano2  4699  nnpredcl  4727  0nelxp  4759  0nelelxp  4760  brab2a  4785  mosubopt  4797  posng  4804  opabssxp  4806  ideqg  4887  relssres  5057  trin2  5135  dminss  5158  iota4an  5314  iota2  5323  iotam  5325  fununfun  5380  fun11uni  5407  imadiflem  5416  funimaexg  5421  fneq12  5430  fvelrnb  5702  dffo4  5803  ffnfv  5813  ffvresb  5818  fmptco  5821  fcoconst  5826  funopsn  5838  fndmexb  5885  fcof1  5934  isotr  5967  isopolem  5973  f1oiso  5977  acexmidlemcase  6023  ovprc1  6065  fnoprabg  6132  elovmporab  6232  elovmporab1w  6233  uchoice  6309  op1steq  6351  dmmpog  6383  1stconst  6395  f1o2ndf1  6402  suppfnss  6435  suppssfvg  6441  brtpos2  6460  tpostpos  6473  tposf12  6478  smores  6501  tfrlemi1  6541  tfr1onlembfn  6553  tfri1dALT  6560  tfrcllembfn  6566  freceq1  6601  freceq2  6602  frectfr  6609  omv2  6676  omsuc  6683  nnsucelsuc  6702  nntri3  6708  nnaordi  6719  nnmordi  6727  nnm00  6741  ecexr  6750  ertr  6760  swoer  6773  erth  6791  ecelqsdm  6817  iinerm  6819  ecinxp  6822  erovlem  6839  pmresg  6888  resixp  6945  elixpsn  6947  mapsnf1o  6949  dom3  6992  modom  7037  mapdom1g  7076  ssenen  7080  phpelm  7096  finexdc  7135  exmidpweq  7144  nnwetri  7151  fiintim  7166  infidc  7176  suppeqfsuppbi  7220  ssfii  7233  fiss  7236  dcfi  7240  supubti  7258  supisoex  7268  ordiso2  7294  inl11  7324  omp1eomlem  7353  nnnninf  7385  nninfisol  7392  ctssexmid  7409  ismkvnex  7414  omniwomnimkv  7426  nninfwlpor  7433  nninfwlpoim  7438  nninfinfwlpo  7439  en2eleq  7466  en2other2  7467  exmidfodomrlemr  7473  exmidfodomrlemrALT  7474  acnrcl  7476  exmidaclem  7483  djuen  7486  djudoml  7494  netap  7533  2omotaplemst  7537  exmidapne  7539  cc1  7544  acnccim  7551  dmaddpqlem  7657  distrnqg  7667  ltanqi  7682  ltmnqi  7683  ltaddnq  7687  ltrnqg  7700  ltnnnq  7703  enq0sym  7712  addnq0mo  7727  mulnq0mo  7728  addnnnq0  7729  distrnq0  7739  prarloclemn  7779  prarloc  7783  ltdfpr  7786  genplt2i  7790  addnqprl  7809  addnqpru  7810  nqprl  7831  appdivnq  7843  1idprl  7870  1idpru  7871  ltexpri  7893  recexpr  7918  cauappcvgprlemdisj  7931  archrecpr  7944  addsrmo  8023  mulsrmo  8024  addsrpr  8025  mulsrpr  8026  0idsr  8047  1idsr  8048  archsr  8062  prsradd  8066  prsrlt  8067  caucvgsr  8082  map2psrprg  8085  elrealeu  8109  muladd11r  8394  negeu  8429  pncan  8444  pncan3  8446  negsub  8486  addid0  8611  posdif  8694  ltnegcon1  8702  subge0  8714  suble0  8715  lesub0  8718  reapval  8815  reapneg  8836  ap0gt0  8879  aprcl  8885  lt0ap0  8887  recextlem1  8890  recapb  8910  div0ap  8941  recrecap  8948  rec11ap  8949  recgt0  9089  mulgt1  9102  lerec2  9128  recp1lt1  9138  recreclt  9139  ledivp1  9142  negiso  9194  nnsub  9241  avglt1  9442  nnrecl  9459  nnnn0addcl  9491  elnn0nn  9503  nn0ge2m1nn  9523  zaddcl  9580  eluzmn  9823  eluzadd  9846  infregelbex  9893  divfnzn  9916  qaddcl  9930  qreccl  9937  cnref1o  9946  ge0p1rp  9981  divlt1lt  10020  divle1le  10021  addlelt  10064  xrre3  10118  xltnegi  10131  xaddval  10141  xaddcom  10157  xnegdi  10164  xposdif  10178  ixxssixx  10198  iccshftr  10290  iccshftl  10292  iccdil  10294  icccntr  10296  zltaddlt1le  10304  elfz2  10312  peano2fzr  10334  fzdcel  10337  fzsplit2  10347  fzaddel  10356  fzrev2  10382  fzrev2i  10383  fzrev3  10384  elfz1b  10387  fseq1p1m1  10391  uzsubfz0  10426  fzosubel3  10504  eluzgtdifelfzo  10505  fzofzp1b  10536  elfzomelpfzo  10539  exfzdc  10549  fvinim0ffz  10550  zsupcllemex  10553  infssuzcldc  10558  exbtwnzlemshrink  10571  qbtwnz  10574  qbtwnxr  10580  ico0  10584  elicore  10589  xqltnle  10590  apbtwnz  10597  flqge  10605  flqlt  10606  flqltnz  10610  flqbi2  10614  flqaddz  10620  flqmulnn0  10622  intfracq  10645  flqdiv  10646  q0mod  10680  q1mod  10681  mulp1mod1  10690  q2txmodxeq0  10709  modfzo0difsn  10720  frec2uzuzd  10727  frec2uzltd  10728  frec2uzrand  10730  uzennn  10761  seqfveq2g  10802  seq3split  10813  seqsplitg  10814  seq3caopr  10820  seqcaoprg  10821  seqf1oglem2  10845  seqf1og  10846  exp3vallem  10865  exp3val  10866  expnnval  10867  exp1  10870  expcl2lemap  10876  rpexpcl  10883  expnegzap  10898  mulexp  10903  mulexpzap  10904  leexp2r  10918  leexp1a  10919  sq11  10937  subsq  10971  binom2  10976  binom3  10982  zesq  10983  bernneq  10985  sq11ap  11032  zzlesq  11033  mulsubdivbinom2ap  11036  apexp1  11043  facwordi  11065  facubnd  11070  facavg  11071  bcval  11074  bcval5  11088  hashennn  11105  fihashf1rn  11113  fseq1hash  11127  hashdifsn  11146  hashdifpr  11147  hashxp  11153  fiubz  11156  fiubnn  11157  fnfz0hash  11159  ffzo0hash  11161  hash2en  11170  wrdval  11182  ffz0iswrdnn0  11206  wrdsymb0  11212  ccatsymb  11245  ccatval21sw  11248  lswccatn0lsw  11254  ccatalpha  11256  ccatrcl1  11257  s111  11274  ccat1st1st  11284  lswccats1fst  11287  swrdlen2  11309  swrdfv2  11310  swrdsbslen  11313  swrds1  11315  ccatswrd  11317  pfxval  11321  pfxclg  11325  pfxmpt  11327  pfxid  11333  pfxfv0  11339  pfxtrcfv0  11341  pfxfvlsw  11342  pfxeq  11343  ccatpfx  11348  swrdpfx  11354  lenrevpfxcctswrd  11359  wrdeqs1cat  11367  cats1un  11368  swrdccatin1  11372  pfxccatin12lem2a  11374  pfxccatin12lem1  11375  pfxccatin12lem3  11379  pfxccatin12  11380  swrdccat  11382  pfxccat3a  11385  swrdccat3blem  11386  swrdccat3b  11387  reuccatpfxs1lem  11393  reuccatpfxs1  11394  s2cl  11432  s2fv0g  11434  shftfvalg  11458  ovshftex  11459  shftdm  11462  shftfib  11463  shftval  11465  shftf  11470  crre  11497  cjexp  11533  cjreim2  11544  uzin2  11627  rexuz3  11630  resqrexlemgt0  11660  resqrex  11666  sqrtgt0  11674  sqrtsq  11684  sqrtmsq  11685  absrpclap  11701  absext  11703  absmul  11709  absid  11711  absexp  11719  nn0abscl  11725  abslt  11728  absle  11729  recvalap  11737  abstri  11744  caubnd2  11757  qdenre  11842  maxabsle  11844  maxabslemval  11848  maxcl  11850  rexanre  11860  min1inf  11872  minabs  11876  minclpr  11877  mul0inf  11881  mingeb  11882  xrmaxiflemcl  11885  xrnegiso  11902  climconst2  11931  climmpt  11940  climres  11943  climcaucn  11991  sumeq1  11995  summodclem2a  12022  isumz  12030  fisumss  12033  fsumzcl2  12046  sumsnf  12050  isumclim3  12064  fsum2dlemstep  12075  fisumcom2  12079  fsumconst  12095  cvgcmpub  12117  binom  12125  binom1p  12126  binom1dif  12128  bcxmas  12130  divcnv  12138  geo2lim  12157  geoisum  12158  geoisumr  12159  geoisum1  12160  mertenslemi1  12176  mertensabs  12178  prod1dc  12227  fprodconst  12261  fprodcom2fi  12267  efcllem  12300  efcj  12314  efadd  12316  efexp  12323  efgt1p2  12336  tanvalap  12349  tanval2ap  12354  tanval3ap  12355  sinadd  12377  cosadd  12378  dvdsdc  12439  iddvdsexp  12456  dvdsadd  12477  dvds1  12494  odd2np1  12514  oddm1even  12516  m1exp1  12542  divalglemnn  12559  fldivndvdslt  12578  flodddiv4lt  12579  bitsp1  12592  bitsmod  12597  bitsfi  12598  bitscmp  12599  bitsinv1lem  12602  dvdsbnd  12607  gcdnncl  12618  zeqzmulgcd  12621  gcdneg  12633  modgcd  12642  bezoutlemex  12652  bezoutlemeu  12658  dfgcd3  12661  gcdzeq  12673  dvdssq  12682  algrf  12697  eucalgval2  12705  eucalgcvga  12710  lcmval  12715  gcddvdslcm  12725  lcmneg  12726  coprmgcdb  12740  qredeu  12749  divgcdcoprm0  12753  divgcdcoprmex  12754  cncongr1  12755  cncongr2  12756  cncongrcoprm  12758  prmind2  12772  dvdsnprmd  12777  exprmfct  12790  isprm6  12799  pw2dvdslemn  12817  oddpwdclemdc  12825  sqrt2irraplemnn  12831  divnumden  12848  divdenle  12849  nn0sqrtelqelz  12858  phivalfi  12864  crth  12876  eulerth  12885  prmdivdiv  12889  reumodprminv  12906  nnnn0modprm0  12908  nnoddn2prmb  12915  pcval  12949  pcidlem  12976  pcid  12977  pcneg  12978  pc2dvds  12983  pcz  12985  pcprod  12999  prmpwdvds  13008  4sqexercise1  13051  2expltfac  13092  xpct  13097  znnen  13099  ennnfonelemg  13104  ennnfone  13126  ctinfom  13129  ctinf  13131  ssomct  13146  isstruct2im  13172  isstruct2r  13173  setsvalg  13192  setsslnid  13214  ressvalsets  13227  ressex  13228  2strbasg  13283  2stropg  13284  2strbas1g  13286  ressmulrg  13308  ressscag  13346  ressvscag  13347  ressipg  13348  restval  13408  restid2  13411  prdsex  13432  pwsval  13454  qusex  13488  fnpr2o  13502  xpsfval  13511  xpsval  13515  intopsn  13530  mgmidmo  13535  lidrididd  13545  ismnddef  13581  mndinvmod  13608  imasmnd2  13615  ismhm  13624  mhmex  13625  insubm  13648  dfgrp2  13690  grpsubval  13709  grpinvinv  13730  grpsubrcan  13744  grpsubadd  13751  grpaddsubass  13753  grpsubsub4  13756  grppnpcan2  13757  grpnpncan  13758  grpnpncan0  13759  grpnnncan2  13760  dfgrp3m  13762  dfgrp3me  13763  imasgrp2  13777  mhmmnd  13783  mulgfvalg  13788  mulgval  13789  mulgfng  13791  mulg1  13796  mulgnnp1  13797  mulgnndir  13818  mulgass  13826  mulgmodid  13828  issubg2m  13856  grpissubg  13861  isnsg  13869  isnsg3  13874  0nsg  13881  eqgfval  13889  eqger  13891  eqgen  13894  eqgcpbl  13895  quseccl  13900  isghm  13910  kerf1ghm  13941  conjghm  13943  conjsubg  13944  abladdsub  13982  ablpncan3  13984  ablsubsub23  13992  invghm  13996  subgabl  13999  mgpress  14025  rngdi  14034  rnglz  14039  imasrng  14050  srgmulgass  14083  srgrmhm  14088  isring  14094  ringo2times  14122  ringrng  14130  ringlz  14137  imasring  14158  opprrng  14171  opprrngbg  14172  opprring  14173  mulgass3  14179  dvdsrd  14189  dvdsrneg  14198  unitnegcl  14225  dvrvald  14229  dvrid  14232  dvr1  14233  dvrass  14234  dvrdir  14238  ringinvdv  14240  rhmex  14252  isrim0  14256  rhmval  14268  rhmdvdsr  14270  rhmopp  14271  elrhmunit  14272  rhmunitinv  14273  isnzr2  14279  ringelnzr  14282  issubrng2  14305  issubrg2  14336  aprap  14382  lmodvs1  14412  lmod0vs  14417  lmodvs0  14418  lmodvsmmulgdi  14419  lmodfopne  14422  lmodvneg1  14426  lss1  14458  islss3  14475  lsslss  14477  lss1d  14479  lspf  14485  lspsn  14512  lspsnneg  14516  sraval  14533  sraring  14545  qus1  14622  qusrhm  14624  cnfldui  14685  dvdsrzring  14699  mulgghm2  14704  mulgrhm  14705  znval  14732  znf1o  14747  psrbagfi  14770  psrbagconcl  14773  psrplusgg  14779  mplgrpfi  14807  eltg2b  14865  difopn  14919  ntrcls0  14942  neii1  14958  restbasg  14979  resttopon  14982  restuni2  14988  cnrest2r  15048  tx1cn  15080  txcnp  15082  txcn  15086  txswaphmeo  15132  psmettri  15141  xmeteq0  15170  xmettri  15183  metrtri  15188  ssblex  15242  xmeter  15247  isxms2  15263  cnbl0  15345  cnblcld  15346  reopnap  15357  tgioo  15365  addcncntoplem  15372  expcn  15380  rescncf  15392  cncfcdm  15393  mulc1cncf  15400  cncfcncntop  15404  addccncf  15411  cdivcncfap  15415  negcncf  15416  cnopnap  15422  suplociccex  15436  hoverlt1  15460  hovergt0  15461  dich0  15463  limccl  15470  ellimc3apf  15471  cnplimcim  15478  limccnp2lem  15487  reldvg  15490  dvbsssg  15497  dvcjbr  15519  dvcj  15520  dvfre  15521  dvrecap  15524  dvef  15538  plyaddcl  15565  plymulcl  15566  plysubcl  15567  plyrecj  15574  reeff1olem  15582  pilem3  15594  ptolemy  15635  rplogcl  15690  rpcxpef  15705  cxprec  15721  rpcxproot  15725  rplogb1  15759  logbgt0b  15777  logbgcd1irr  15778  binom4  15790  wilthlem1  15794  sgmnncl  15802  dvdsppwf1o  15803  mersenne  15811  lgslem4  15822  lgsval  15823  lgsval2lem  15829  lgsval4a  15841  lgsdir2lem3  15849  lgsdir2  15852  lgsne0  15857  lgsprme0  15861  lgsmulsqcoprm  15865  gausslemma2dlem0a  15868  gausslemma2dlem1a  15877  2lgslem1b  15908  2lgslem2  15911  2lgsoddprm  15932  struct2slots2dom  15979  structvtxval  15980  structiedg0val  15981  struct2griedg  15987  edgstruct  16005  uhgr0vb  16025  incistruhgr  16031  umgrvad2edg  16152  uspgredg2vlem  16161  uspgredg2v  16162  usgredg2v  16165  ushgredgedg  16167  ushgredgedgloop  16169  usgr0vb  16174  uhgr0vusgr  16179  edg0usgr  16188  subupgr  16214  upgrspanop  16224  umgrspanop  16225  usgrspanop  16226  vtxdgfval  16229  wksfval  16263  wlkpropg  16265  uspgr2wlkeq2  16307  uspgr2wlkeqi  16308  upgr2wlkdc  16318  trlsex  16328  clwwlkccatlem  16341  clwwlkng  16346  clwwlkext2edg  16363  clwwlknccat  16364  umgr2cwwkdifex  16366  clwwlknonel  16373  clwwlknonccat  16374  clwwlknonex2lem2  16379  clwwlknun  16382  eupthsg  16386  eupth2lem3lem6fi  16412  bj-nnan  16454  bj-indind  16648  bj-omtrans  16672  bj-inf2vnlem1  16686  sscoll2  16704  2omap  16715  pw1map  16717  pwtrufal  16719  sssneq  16724  pw1nct  16725  exmidnotnotr  16727  nninfsellemsuc  16738  nninfomnilem  16744  nnnninfex  16748  exmidsbthrlem  16750  qdencn  16755  trilpo  16775  trirec0  16776  apdiff  16780  iswomninnlem  16782  iswomni0  16784  redcwlpo  16788  redc0  16790  reap0  16791  cndcap  16792  dceqnconst  16793  dcapnconst  16794  neapmkv  16801  neap0mkv  16802