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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-ia1 106

This theorem is used by:  simpli  111  simpld  112  imp  124  adantrd  279  iba  300  pm3.41  331  pm4.45im  334  anim12  344  pm4.71  393  adantlr  481  adantrr  483  adantllr  485  adantlrr  487  adantrlr  489  adantrrr  491  simplll  539  simplrl  541  simprll  543  simprrl  545  anabs1  578  jcab  611  pm4.38  613  pm5.21  707  ioran  764  pm3.14  765  pm4.44  791  ordi  828  pm4.39  834  animorl  835  animorlr  837  pm5.16  840  pm5.54dc  930  intnanr  942  intnanrd  944  dcan  946  dedlema  982  dedlemb  983  pm4.42r  984  prlem2  987  ifpdc  992  dfifp2dc  994  simp1l  1052  simp2l  1054  simp3l  1056  3anandis  1388  xordc1  1442  anxordi  1449  falantru  1452  19.26  1534  exsimpl  1670  sbequ2  1822  sbcof2  1863  sbequilem  1891  sbequ8  1900  euan  2143  mooran1  2159  eupickbi  2169  2exeu  2179  dimatis  2204  rexim  2644  r19.26  2677  r19.40  2705  rspcime  2937  rr19.28v  2966  elrab3t  2981  eueq3dc  3000  mosubt  3003  reu6  3015  sbc2iegf  3122  sbcralt  3128  sbcrext  3129  rmob  3145  csbiebt  3187  ssab2  3332  difdif  3354  uneqin  3482  indifdir  3487  undif3ss  3492  abanssl  3501  rexm  3627  eqifdc  3677  ifandc  3681  ifnebibdc  3686  difsn  3852  opprc1  3926  unissel  3964  ssmin  3989  abssexg  4319  undifexmid  4330  pwntru  4336  exmidundif  4343  exmidundifim  4344  opelopabsb  4402  elopabran  4426  sess1  4482  ordelord  4526  onin  4531  suctr  4566  abnexg  4592  ifexg  4631  ordtriexmidlem  4666  ordtri2or2exmid  4718  ontri2orexmidim  4719  tfi  4729  peano1  4741  peano2  4742  nnpredcl  4770  0nelxp  4802  0nelelxp  4803  brab2a  4828  mosubopt  4840  posng  4847  opabssxp  4849  ideqg  4931  relssres  5101  trin2  5179  dminss  5202  iota4an  5358  iota2  5367  iotam  5369  fununfun  5424  fun11uni  5451  imadiflem  5460  funimaexg  5465  fneq12  5474  fvelrnb  5750  dffo4  5856  ffnfv  5866  ffvresb  5871  fmptco  5874  fcoconst  5879  funopsn  5891  fndmexb  5938  mptmex  5945  fcof1  5989  isotr  6022  isopolem  6028  f1oiso  6032  acexmidlemcase  6080  ovprc1  6122  fnoprabg  6189  elovmporab  6289  elovmporab1w  6290  uchoice  6371  op1steq  6413  dmmpog  6445  1stconst  6457  f1o2ndf1  6464  suppfnss  6497  suppssfvg  6503  brtpos2  6522  tpostpos  6535  tposf12  6540  smores  6563  tfrlemi1  6603  tfr1onlembfn  6615  tfri1dALT  6622  tfrcllembfn  6628  freceq1  6663  freceq2  6664  frectfr  6671  omv2  6738  omsuc  6745  nnsucelsuc  6764  nntri3  6770  nnaordi  6781  nnmordi  6789  nnm00  6803  ecexr  6812  ertr  6822  swoer  6835  erth  6853  ecelqsdm  6879  iinerm  6881  ecinxp  6884  erovlem  6901  pmresg  6957  resixp  7015  elixpsn  7017  mapsnf1o  7019  dom3  7062  modom  7108  mapdom1g  7147  ssenen  7152  phpelm  7168  finexdc  7207  exmidpweq  7216  nnwetri  7223  fiintim  7238  infidc  7248  suppeqfsuppbi  7295  ssfii  7308  fiss  7311  dcfi  7315  2omap  7319  supubti  7340  supisoex  7350  ordiso2  7376  inl11  7406  omp1eomlem  7435  nnnninf  7467  nninfisol  7474  ctssexmid  7491  ismkvnex  7496  omniwomnimkv  7508  nninfwlpor  7515  nninfwlpoim  7520  nninfinfwlpo  7521  en2eleq  7548  en2other2  7549  exmidfodomrlemr  7555  exmidfodomrlemrALT  7556  acnrcl  7558  exmidaclem  7565  djuen  7568  djudoml  7576  netap  7621  2omotaplemst  7625  exmidapne  7627  cc1  7632  acnccim  7639  dmaddpqlem  7745  distrnqg  7755  ltanqi  7770  ltmnqi  7771  ltaddnq  7775  ltrnqg  7788  ltnnnq  7791  enq0sym  7800  addnq0mo  7815  mulnq0mo  7816  addnnnq0  7817  distrnq0  7827  prarloclemn  7867  prarloc  7871  ltdfpr  7874  genplt2i  7878  addnqprl  7897  addnqpru  7898  nqprl  7919  appdivnq  7931  1idprl  7958  1idpru  7959  ltexpri  7981  recexpr  8006  cauappcvgprlemdisj  8019  archrecpr  8032  addsrmo  8111  mulsrmo  8112  addsrpr  8113  mulsrpr  8114  0idsr  8135  1idsr  8136  archsr  8150  prsradd  8154  prsrlt  8155  caucvgsr  8170  map2psrprg  8173  elrealeu  8197  muladd11r  8484  negeu  8519  pncan  8534  pncan3  8536  negsub  8576  addid0  8701  addeq0  8705  posdif  8785  ltnegcon1  8793  subge0  8805  suble0  8806  lesub0  8809  reapval  8907  reapneg  8928  ap0gt0  8971  aprcl  8977  lt0ap0  8979  recextlem1  8982  recapb  9004  div0ap  9035  recrecap  9042  rec11ap  9043  recgt0  9183  mulgt1  9196  lerec2  9222  recp1lt1  9232  recreclt  9233  ledivp1  9236  negiso  9288  nnsub  9346  avglt1  9549  nnrecl  9566  nnnn0addcl  9598  elnn0nn  9610  fcdmnn0fsuppg  9623  nn0ge2m1nn  9632  zaddcl  9689  eluzmn  9938  eluzadd  9961  infregelbex  10008  divfnzn  10031  qaddcl  10045  qreccl  10052  cnref1o  10062  ge0p1rp  10097  divlt1lt  10136  divle1le  10137  addlelt  10180  xrre3  10235  xltnegi  10248  xaddval  10258  xaddcom  10274  xnegdi  10281  xposdif  10295  ixxssixx  10315  iccshftr  10407  iccshftl  10409  iccdil  10411  icccntr  10413  zltaddlt1le  10421  elfz2  10429  peano2fzr  10452  fzdcel  10455  fzsplit2  10466  fzaddel  10476  fzrev2  10503  fzrev2i  10504  fzrev3  10505  elfz1b  10508  fseq1p1m1  10512  uzsubfz0  10547  fzosubel3  10625  eluzgtdifelfzo  10626  fzofzp1b  10657  elfzomelpfzo  10660  exfzdc  10670  fvinim0ffz  10671  zsupcllemex  10674  infssuzcldc  10679  exbtwnzlemshrink  10694  qbtwnz  10697  qbtwnxr  10703  ico0  10707  elicore  10712  xqltnle  10713  apbtwnz  10720  flaplelt  10724  flqge  10730  flapge  10731  flqlt  10732  flqltnz  10737  flqbi2  10741  flqaddz  10747  flqmulnn0  10749  intfracq  10772  flqdiv  10773  q0mod  10807  q1mod  10808  mulp1mod1  10817  q2txmodxeq0  10836  modfzo0difsn  10847  frec2uzuzd  10854  frec2uzltd  10855  frec2uzrand  10857  uzennn  10888  seqfveq2g  10929  seq3split  10940  seqsplitg  10941  seq3caopr  10947  seqcaoprg  10948  seqf1oglem2  10972  seqf1og  10973  exp3vallem  10992  exp3val  10993  expnnval  10994  exp1  10997  expcl2lemap  11003  rpexpcl  11010  expnegzap  11025  mulexp  11030  mulexpzap  11031  leexp2r  11045  leexp1a  11046  sq11  11064  subsq  11098  binom2  11103  binom3  11109  zesq  11111  bernneq  11113  sq11ap  11160  zzlesq  11161  mulsubdivbinom2ap  11165  apexp1  11172  facwordi  11194  facubnd  11199  facavg  11200  bcval  11203  bcval5  11217  hashennn  11235  fihashf1rn  11243  fseq1hash  11257  hashdifsn  11276  hashdifpr  11277  hashxp  11283  hashmap  11284  fiubz  11288  fiubnn  11289  fnfz0hash  11291  ffzo0hash  11293  ssenneg  11296  hashfibclem  11298  hashf1  11303  hash2en  11311  wrdval  11323  ffz0iswrdnn0  11347  wrdsymb0  11353  ccatsymb  11386  ccatval21sw  11389  lswccatn0lsw  11395  ccatalpha  11397  ccatrcl1  11398  s111  11415  ccat1st1st  11425  lswccats1fst  11428  swrdlen2  11450  swrdfv2  11451  swrdsbslen  11454  swrds1  11456  ccatswrd  11458  pfxval  11462  pfxclg  11466  pfxmpt  11468  pfxid  11474  pfxfv0  11480  pfxtrcfv0  11482  pfxfvlsw  11483  pfxeq  11484  ccatpfx  11489  swrdpfx  11495  lenrevpfxcctswrd  11500  wrdeqs1cat  11508  cats1un  11509  swrdccatin1  11513  pfxccatin12lem2a  11515  pfxccatin12lem1  11516  pfxccatin12lem3  11520  pfxccatin12  11521  swrdccat  11523  pfxccat3a  11526  swrdccat3blem  11527  swrdccat3b  11528  reuccatpfxs1lem  11534  reuccatpfxs1  11535  s2cl  11573  s2fv0g  11575  shftfvalg  11599  ovshftex  11600  shftdm  11603  shftfib  11604  shftval  11606  shftf  11611  crre  11638  cjexp  11674  cjreim2  11686  uzin2  11769  rexuz3  11772  resqrexlemgt0  11802  resqrex  11808  sqrtgt0  11816  sqrtsq  11826  sqrtmsq  11827  absrpclap  11843  absext  11845  absmul  11851  absid  11853  qabscl  11859  absexp  11862  nn0abscl  11868  abslt  11871  absle  11872  recvalap  11880  abstri  11887  caubnd2  11900  qdenre  11985  maxabsle  11987  maxabslemval  11991  maxcl  11993  rexanre  12003  min1inf  12016  minabs  12020  minclpr  12021  mul0inf  12026  mingeb  12027  xrmaxiflemcl  12030  xrnegiso  12047  climconst2  12076  climmpt  12085  climres  12088  climcaucn  12136  sumeq1  12140  summodclem2a  12167  isumz  12175  fisumss  12178  fsumzcl2  12191  sumsnf  12195  isumclim3  12209  fsum2dlemstep  12220  fisumcom2  12224  fsumconst  12240  cvgcmpub  12262  binom  12270  binom1p  12271  binom1dif  12273  bcxmas  12275  divcnv  12283  geo2lim  12302  geoisum  12303  geoisumr  12304  geoisum1  12305  mertenslemi1  12321  mertensabs  12323  prod1dc  12372  fprodconst  12406  fprodcom2fi  12412  efcllem  12445  efcj  12459  efadd  12461  efexp  12468  efgt1p2  12481  tanvalap  12494  tanval2ap  12499  tanval3ap  12500  sinadd  12522  cosadd  12523  dvdsdc  12584  iddvdsexp  12601  dvdsadd  12622  dvds1  12639  odd2np1  12659  oddm1even  12661  m1exp1  12687  divalglemnn  12704  fldivndvdslt  12723  flodddiv4lt  12724  bitsp1  12737  bitsmod  12742  bitsfi  12743  bitscmp  12744  bitsinv1lem  12747  dvdsbnd  12752  gcdnncl  12763  zeqzmulgcd  12766  gcdneg  12778  modgcd  12787  bezoutlemex  12797  bezoutlemeu  12803  dfgcd3  12806  gcdzeq  12818  dvdssq  12827  algrf  12842  eucalgval2  12850  eucalgcvga  12855  lcmval  12860  gcddvdslcm  12870  lcmneg  12871  coprmgcdb  12885  qredeu  12894  divgcdcoprm0  12898  divgcdcoprmex  12899  cncongr1  12900  cncongr2  12901  cncongrcoprm  12903  prmind2  12917  dvdsnprmd  12922  exprmfct  12936  isprm6  12945  pwbdvds  12964  nnmaxpwlemnfac  12970  nnmaxpwlemparts  12971  nnmaxpw  12972  sqrt2irraplemnn  12978  divnumden  12995  divdenle  12996  nn0sqrtelqelz  13005  phivalfi  13013  crth  13025  eulerth  13034  prmdivdiv  13038  reumodprminv  13055  nnnn0modprm0  13057  nnoddn2prmb  13064  pcval  13098  pcidlem  13125  pcid  13126  pcneg  13127  pc2dvds  13132  pcz  13134  pcprod  13148  prmpwdvds  13157  4sqexercise1  13200  2expltfac  13242  prmlem0  13243  ballotfilemfval  13281  ballotfilemefi  13289  ballotfilemodife  13292  ballotfilem4  13293  ballotfilemsval  13304  ballotfilemieq  13312  ballotfilemrv  13315  ballotfilemrinv0  13328  xpct  13339  znnen  13341  ennnfonelemg  13346  ennnfone  13368  ctinfom  13371  ctinf  13373  ssomct  13388  isstruct2im  13414  isstruct2r  13415  setsvalg  13434  setsslnid  13456  ressvalsets  13470  ressex  13471  2strbasg  13527  2stropg  13528  2strbas1g  13530  ressmulrg  13552  ressscag  13590  ressvscag  13591  ressipg  13592  restval  13652  restid2  13655  qusex  13699  fnpr2o  13713  xpsfval  13722  intopsn  13740  mgmidmo  13745  lidrididd  13755  ismnddef  13784  mndinvmod  13811  imasmnd2  13812  ismhm  13821  mhmex  13822  insubm  13845  dfgrp2  13885  grpsubval  13904  grpinvinv  13925  grpsubrcan  13939  grpsubadd  13946  grpaddsubass  13948  grpsubsub4  13951  grppnpcan2  13952  grpnpncan  13953  grpnpncan0  13954  grpnnncan2  13955  dfgrp3m  13957  dfgrp3me  13958  imasgrp2  13966  mhmmnd  13972  mulgfvalg  13977  mulgval  13978  mulgfng  13980  mulg1  13985  mulgnnp1  13986  mulgnndir  14007  mulgass  14015  mulgmodid  14017  issubg2m  14045  grpissubg  14050  isnsg  14058  isnsg3  14063  0nsg  14070  eqgfval  14078  eqger  14080  eqgen  14083  eqgcpbl  14084  quseccl  14089  isghm  14099  kerf1ghm  14130  conjghm  14132  conjsubg  14133  cntzval  14147  cntzidss  14166  cntrsubgnsg  14169  abladdsub  14203  ablpncan3  14205  ablsubsub23  14213  invghm  14217  subgabl  14220  prdsex  14256  xpsval  14285  pwsval  14288  mgpress  14314  rngdi  14323  rnglz  14328  imasrng  14339  srgmulgass  14377  srgrmhm  14382  isring  14388  ringo2times  14417  ringrng  14425  ringlz  14432  imasring  14453  opprrng  14466  opprrngbg  14467  opprring  14468  mulgass3  14475  dvdsrd  14485  dvdsrneg  14494  unitnegcl  14521  dvrvald  14525  dvrid  14528  dvr1  14529  dvrass  14530  dvrdir  14534  ringinvdv  14536  rhmex  14548  isrim0  14552  rhmval  14564  rhmdvdsr  14566  rhmopp  14567  elrhmunit  14568  rhmunitinv  14569  isnzr2  14575  ringelnzr  14578  issubrng2  14602  issubrg2  14633  ringunitap  14677  aprap  14682  aprnzr  14683  opprdrng  14704  lmodvs1  14737  lmod0vs  14742  lmodvs0  14743  lmodvsmmulgdi  14744  lmodfopne  14747  lmodvneg1  14751  lss1  14783  islss3  14800  lsslss  14802  lss1d  14804  lspf  14810  lspsn  14837  lspsnneg  14841  sraval  14858  sraring  14870  qus1  14947  qusrhm  14949  cnfldui  15008  dvdsrzring  15022  mulgghm2  15027  mulgrhm  15028  znval  15055  znf1o  15070  assa2ass  15093  assa2ass2  15094  issubassa3  15096  assamulgscmlem2  15126  psrbagfi  15143  psrbaglefifi  15147  psrbagconcl  15148  psrplusgg  15154  psrmulrg  15158  mplgrpfi  15188  eltg2b  15246  difopn  15300  ntrcls0  15323  neii1  15339  restbasg  15360  resttopon  15363  restuni2  15369  cnrest2r  15429  tx1cn  15461  txcnp  15463  txcn  15467  txswaphmeo  15513  psmettri  15522  xmeteq0  15551  xmettri  15564  metrtri  15569  ssblex  15623  xmeter  15628  isxms2  15644  cnbl0  15726  cnblcld  15727  reopnap  15738  tgioo  15746  addcncntoplem  15753  expcn  15761  rescncf  15773  cncfcdm  15774  mulc1cncf  15781  cncfcncntop  15785  addccncf  15792  cdivcncfap  15796  negcncf  15797  cnopnap  15803  suplociccex  15817  hoverlt1  15841  hovergt0  15842  dich0  15844  limccl  15851  ellimc3apf  15852  cnplimcim  15859  limccnp2lem  15868  reldvg  15871  dvbsssg  15878  dvcjbr  15900  dvcj  15901  dvfre  15902  dvrecap  15905  dvef  15919  plyaddcl  15946  plymulcl  15947  plysubcl  15948  plyrecj  15955  reeff1olem  15963  pilem3  15976  ptolemy  16017  rplogcl  16073  rpcxpef  16091  cxprec  16107  rpcxproot  16111  rplogb1  16145  logbgt0b  16163  logbgcd1irr  16164  zprmlogbaplem3  16178  binom4  16180  birthdaylem1g  16186  wilthlem1  16193  sgmnncl  16218  ppiprm  16220  dvdsppwf1o  16244  ppiublem1  16252  ppiqub  16254  chtublem  16256  chtqub  16257  mersenne  16258  lgslem4  16288  lgsval  16289  lgsval2lem  16295  lgsval4a  16307  lgsdir2lem3  16315  lgsdir2  16318  lgsne0  16323  lgsprme0  16327  lgsmulsqcoprm  16331  gausslemma2dlem0a  16334  gausslemma2dlem1a  16343  2lgslem1b  16374  2lgslem2  16377  2lgsoddprm  16398  struct2slots2dom  16445  structvtxval  16446  structiedg0val  16447  struct2griedg  16453  edgstruct  16471  uhgr0vb  16491  incistruhgr  16497  umgrvad2edg  16618  uspgredg2vlem  16627  uspgredg2v  16628  usgredg2v  16631  ushgredgedg  16633  ushgredgedgloop  16635  usgr0vb  16640  uhgr0vusgr  16645  edg0usgr  16654  subupgr  16680  upgrspanop  16690  umgrspanop  16691  usgrspanop  16692  vtxdgfval  16695  wksfval  16729  wlkpropg  16731  uspgr2wlkeq2  16773  uspgr2wlkeqi  16774  upgr2wlkdc  16784  trlsex  16794  clwwlkccatlem  16807  clwwlkng  16812  clwwlkext2edg  16829  clwwlknccat  16830  umgr2cwwkdifex  16832  clwwlknonel  16839  clwwlknonccat  16840  clwwlknonex2lem2  16845  clwwlknun  16848  eupthsg  16852  eupth2lem3lem6fi  16878  dichmul0orlem7  16925  dichmul0or  16926  bj-nnan  16930  bj-indind  17124  bj-omtrans  17148  bj-inf2vnlem1  17162  sscoll2  17180  pw1map  17191  pwtrufal  17193  sssneq  17198  pw1nct  17199  exmidnotnotr  17202  nninfsellemsuc  17221  nninfomnilem  17227  nnnninfex  17231  exmidsbthrlem  17233  qdencn  17238  trilpo  17259  trirec0  17260  apdiff  17264  iswomninnlem  17266  iswomni0  17268  redcwlpo  17272  redc0  17274  reap0  17275  cndcap  17276  dceqnconst  17277  dcapnconst  17278  neapmkv  17285  neap0mkv  17286  als-no-surprise  17314