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  605  pm4.38  607  pm5.21  700  ioran  757  pm3.14  758  pm4.44  784  ordi  821  pm4.39  827  animorl  828  animorlr  830  pm5.16  833  pm5.54dc  923  intnanr  935  intnanrd  937  dcan  939  dedlema  975  dedlemb  976  pm4.42r  977  prlem2  980  ifpdc  985  dfifp2dc  987  simp1l  1045  simp2l  1047  simp3l  1049  3anandis  1381  xordc1  1435  anxordi  1442  falantru  1445  19.26  1527  exsimpl  1663  sbequ2  1815  sbcof2  1856  sbequilem  1884  sbequ8  1893  euan  2134  mooran1  2150  eupickbi  2160  2exeu  2170  dimatis  2195  rexim  2624  r19.26  2657  r19.40  2685  rspcime  2914  rr19.28v  2943  elrab3t  2958  eueq3dc  2977  mosubt  2980  reu6  2992  sbc2iegf  3099  sbcralt  3105  sbcrext  3106  rmob  3122  csbiebt  3164  ssab2  3308  difdif  3329  uneqin  3455  indifdir  3460  undif3ss  3465  rexm  3591  eqifdc  3639  ifandc  3643  ifnebibdc  3648  difsn  3805  opprc1  3879  unissel  3917  ssmin  3942  abssexg  4266  undifexmid  4277  pwntru  4283  exmidundif  4290  exmidundifim  4291  opelopabsb  4348  elopabran  4372  sess1  4428  ordelord  4472  onin  4477  suctr  4512  abnexg  4537  ifexg  4576  ordtriexmidlem  4611  ordtri2or2exmid  4663  ontri2orexmidim  4664  tfi  4674  peano1  4686  peano2  4687  nnpredcl  4715  0nelxp  4747  0nelelxp  4748  brab2a  4772  mosubopt  4784  posng  4791  opabssxp  4793  ideqg  4873  relssres  5043  trin2  5120  dminss  5143  iota4an  5299  iota2  5308  iotam  5310  fununfun  5364  fun11uni  5391  imadiflem  5400  funimaexg  5405  fneq12  5414  fvelrnb  5683  dffo4  5785  ffnfv  5795  ffvresb  5800  fmptco  5803  fcoconst  5808  funopsn  5819  fcof1  5913  isotr  5946  isopolem  5952  f1oiso  5956  acexmidlemcase  6002  ovprc1  6044  fnoprabg  6111  elovmporab  6211  elovmporab1w  6212  uchoice  6289  op1steq  6331  dmmpog  6361  1stconst  6373  f1o2ndf1  6380  brtpos2  6403  tpostpos  6416  tposf12  6421  smores  6444  tfrlemi1  6484  tfr1onlembfn  6496  tfri1dALT  6503  tfrcllembfn  6509  freceq1  6544  freceq2  6545  frectfr  6552  omv2  6619  omsuc  6626  nnsucelsuc  6645  nntri3  6651  nnaordi  6662  nnmordi  6670  nnm00  6684  ecexr  6693  ertr  6703  swoer  6716  erth  6734  ecelqsdm  6760  iinerm  6762  ecinxp  6765  erovlem  6782  pmresg  6831  resixp  6888  elixpsn  6890  mapsnf1o  6892  dom3  6935  mapdom1g  7016  ssenen  7020  phpelm  7036  finexdc  7073  exmidpweq  7082  nnwetri  7089  fiintim  7104  infidc  7112  ssfii  7152  fiss  7155  dcfi  7159  supubti  7177  supisoex  7187  ordiso2  7213  inl11  7243  omp1eomlem  7272  nnnninf  7304  nninfisol  7311  ctssexmid  7328  ismkvnex  7333  omniwomnimkv  7345  nninfwlpor  7352  nninfwlpoim  7357  nninfinfwlpo  7358  en2eleq  7384  en2other2  7385  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  acnrcl  7394  exmidaclem  7401  djuen  7404  djudoml  7412  netap  7451  2omotaplemst  7455  exmidapne  7457  cc1  7462  acnccim  7469  dmaddpqlem  7575  distrnqg  7585  ltanqi  7600  ltmnqi  7601  ltaddnq  7605  ltrnqg  7618  ltnnnq  7621  enq0sym  7630  addnq0mo  7645  mulnq0mo  7646  addnnnq0  7647  distrnq0  7657  prarloclemn  7697  prarloc  7701  ltdfpr  7704  genplt2i  7708  addnqprl  7727  addnqpru  7728  nqprl  7749  appdivnq  7761  1idprl  7788  1idpru  7789  ltexpri  7811  recexpr  7836  cauappcvgprlemdisj  7849  archrecpr  7862  addsrmo  7941  mulsrmo  7942  addsrpr  7943  mulsrpr  7944  0idsr  7965  1idsr  7966  archsr  7980  prsradd  7984  prsrlt  7985  caucvgsr  8000  map2psrprg  8003  elrealeu  8027  muladd11r  8313  negeu  8348  pncan  8363  pncan3  8365  negsub  8405  addid0  8530  posdif  8613  ltnegcon1  8621  subge0  8633  suble0  8634  lesub0  8637  reapval  8734  reapneg  8755  ap0gt0  8798  aprcl  8804  lt0ap0  8806  recextlem1  8809  recapb  8829  div0ap  8860  recrecap  8867  rec11ap  8868  recgt0  9008  mulgt1  9021  lerec2  9047  recp1lt1  9057  recreclt  9058  ledivp1  9061  negiso  9113  nnsub  9160  avglt1  9361  nnrecl  9378  nnnn0addcl  9410  elnn0nn  9422  nn0ge2m1nn  9440  zaddcl  9497  eluzmn  9740  eluzadd  9763  infregelbex  9805  divfnzn  9828  qaddcl  9842  qreccl  9849  cnref1o  9858  ge0p1rp  9893  divlt1lt  9932  divle1le  9933  addlelt  9976  xrre3  10030  xltnegi  10043  xaddval  10053  xaddcom  10069  xnegdi  10076  xposdif  10090  ixxssixx  10110  iccshftr  10202  iccshftl  10204  iccdil  10206  icccntr  10208  zltaddlt1le  10215  elfz2  10223  peano2fzr  10245  fzdcel  10248  fzsplit2  10258  fzaddel  10267  fzrev2  10293  fzrev2i  10294  fzrev3  10295  elfz1b  10298  fseq1p1m1  10302  uzsubfz0  10337  fzosubel3  10414  eluzgtdifelfzo  10415  fzofzp1b  10446  elfzomelpfzo  10449  exfzdc  10458  fvinim0ffz  10459  zsupcllemex  10462  infssuzcldc  10467  exbtwnzlemshrink  10480  qbtwnz  10483  qbtwnxr  10489  ico0  10493  elicore  10498  xqltnle  10499  apbtwnz  10506  flqge  10514  flqlt  10515  flqltnz  10519  flqbi2  10523  flqaddz  10529  flqmulnn0  10531  intfracq  10554  flqdiv  10555  q0mod  10589  q1mod  10590  mulp1mod1  10599  q2txmodxeq0  10618  modfzo0difsn  10629  frec2uzuzd  10636  frec2uzltd  10637  frec2uzrand  10639  uzennn  10670  seqfveq2g  10711  seq3split  10722  seqsplitg  10723  seq3caopr  10729  seqcaoprg  10730  seqf1oglem2  10754  seqf1og  10755  exp3vallem  10774  exp3val  10775  expnnval  10776  exp1  10779  expcl2lemap  10785  rpexpcl  10792  expnegzap  10807  mulexp  10812  mulexpzap  10813  leexp2r  10827  leexp1a  10828  sq11  10846  subsq  10880  binom2  10885  binom3  10891  zesq  10892  bernneq  10894  sq11ap  10941  zzlesq  10942  mulsubdivbinom2ap  10945  apexp1  10952  facwordi  10974  facubnd  10979  facavg  10980  bcval  10983  bcval5  10997  hashennn  11014  fihashf1rn  11022  fseq1hash  11035  hashdifsn  11054  hashdifpr  11055  hashxp  11061  fiubz  11064  fiubnn  11065  fnfz0hash  11067  ffzo0hash  11069  hash2en  11078  wrdval  11087  ffz0iswrdnn0  11111  wrdsymb0  11117  ccatsymb  11150  ccatval21sw  11153  lswccatn0lsw  11159  ccatalpha  11161  ccatrcl1  11162  s111  11179  ccat1st1st  11188  lswccats1fst  11191  swrdlen2  11210  swrdfv2  11211  swrdsbslen  11214  swrds1  11216  ccatswrd  11218  pfxval  11222  pfxclg  11226  pfxmpt  11228  pfxid  11234  pfxfv0  11240  pfxtrcfv0  11242  pfxfvlsw  11243  pfxeq  11244  ccatpfx  11249  swrdpfx  11255  lenrevpfxcctswrd  11260  wrdeqs1cat  11268  cats1un  11269  swrdccatin1  11273  pfxccatin12lem2a  11275  pfxccatin12lem1  11276  pfxccatin12lem3  11280  pfxccatin12  11281  swrdccat  11283  pfxccat3a  11286  swrdccat3blem  11287  swrdccat3b  11288  reuccatpfxs1lem  11294  reuccatpfxs1  11295  s2cl  11333  s2fv0g  11335  shftfvalg  11345  ovshftex  11346  shftdm  11349  shftfib  11350  shftval  11352  shftf  11357  crre  11384  cjexp  11420  cjreim2  11431  uzin2  11514  rexuz3  11517  resqrexlemgt0  11547  resqrex  11553  sqrtgt0  11561  sqrtsq  11571  sqrtmsq  11572  absrpclap  11588  absext  11590  absmul  11596  absid  11598  absexp  11606  nn0abscl  11612  abslt  11615  absle  11616  recvalap  11624  abstri  11631  caubnd2  11644  qdenre  11729  maxabsle  11731  maxabslemval  11735  maxcl  11737  rexanre  11747  min1inf  11759  minabs  11763  minclpr  11764  mul0inf  11768  mingeb  11769  xrmaxiflemcl  11772  xrnegiso  11789  climconst2  11818  climmpt  11827  climres  11830  climcaucn  11878  sumeq1  11882  summodclem2a  11908  isumz  11916  fisumss  11919  fsumzcl2  11932  sumsnf  11936  isumclim3  11950  fsum2dlemstep  11961  fisumcom2  11965  fsumconst  11981  cvgcmpub  12003  binom  12011  binom1p  12012  binom1dif  12014  bcxmas  12016  divcnv  12024  geo2lim  12043  geoisum  12044  geoisumr  12045  geoisum1  12046  mertenslemi1  12062  mertensabs  12064  prod1dc  12113  fprodconst  12147  fprodcom2fi  12153  efcllem  12186  efcj  12200  efadd  12202  efexp  12209  efgt1p2  12222  tanvalap  12235  tanval2ap  12240  tanval3ap  12241  sinadd  12263  cosadd  12264  dvdsdc  12325  iddvdsexp  12342  dvdsadd  12363  dvds1  12380  odd2np1  12400  oddm1even  12402  m1exp1  12428  divalglemnn  12445  fldivndvdslt  12464  flodddiv4lt  12465  bitsp1  12478  bitsmod  12483  bitsfi  12484  bitscmp  12485  bitsinv1lem  12488  dvdsbnd  12493  gcdnncl  12504  zeqzmulgcd  12507  gcdneg  12519  modgcd  12528  bezoutlemex  12538  bezoutlemeu  12544  dfgcd3  12547  gcdzeq  12559  dvdssq  12568  algrf  12583  eucalgval2  12591  eucalgcvga  12596  lcmval  12601  gcddvdslcm  12611  lcmneg  12612  coprmgcdb  12626  qredeu  12635  divgcdcoprm0  12639  divgcdcoprmex  12640  cncongr1  12641  cncongr2  12642  cncongrcoprm  12644  prmind2  12658  dvdsnprmd  12663  exprmfct  12676  isprm6  12685  pw2dvdslemn  12703  oddpwdclemdc  12711  sqrt2irraplemnn  12717  divnumden  12734  divdenle  12735  nn0sqrtelqelz  12744  phivalfi  12750  crth  12762  eulerth  12771  prmdivdiv  12775  reumodprminv  12792  nnnn0modprm0  12794  nnoddn2prmb  12801  pcval  12835  pcidlem  12862  pcid  12863  pcneg  12864  pc2dvds  12869  pcz  12871  pcprod  12885  prmpwdvds  12894  4sqexercise1  12937  2expltfac  12978  xpct  12983  znnen  12985  ennnfonelemg  12990  ennnfone  13012  ctinfom  13015  ctinf  13017  ssomct  13032  isstruct2im  13058  isstruct2r  13059  setsvalg  13078  setsslnid  13100  ressvalsets  13113  ressex  13114  2strbasg  13169  2stropg  13170  2strbas1g  13172  ressmulrg  13194  ressscag  13232  ressvscag  13233  ressipg  13234  restval  13294  restid2  13297  prdsex  13318  pwsval  13340  qusex  13374  fnpr2o  13388  xpsfval  13397  xpsval  13401  intopsn  13416  mgmidmo  13421  lidrididd  13431  ismnddef  13467  mndinvmod  13494  imasmnd2  13501  ismhm  13510  mhmex  13511  insubm  13534  dfgrp2  13576  grpsubval  13595  grpinvinv  13616  grpsubrcan  13630  grpsubadd  13637  grpaddsubass  13639  grpsubsub4  13642  grppnpcan2  13643  grpnpncan  13644  grpnpncan0  13645  grpnnncan2  13646  dfgrp3m  13648  dfgrp3me  13649  imasgrp2  13663  mhmmnd  13669  mulgfvalg  13674  mulgval  13675  mulgfng  13677  mulg1  13682  mulgnnp1  13683  mulgnndir  13704  mulgass  13712  mulgmodid  13714  issubg2m  13742  grpissubg  13747  isnsg  13755  isnsg3  13760  0nsg  13767  eqgfval  13775  eqger  13777  eqgen  13780  eqgcpbl  13781  quseccl  13786  isghm  13796  kerf1ghm  13827  conjghm  13829  conjsubg  13830  abladdsub  13868  ablpncan3  13870  ablsubsub23  13878  invghm  13882  subgabl  13885  mgpress  13910  rngdi  13919  rnglz  13924  imasrng  13935  srgmulgass  13968  srgrmhm  13973  isring  13979  ringo2times  14007  ringrng  14015  ringlz  14022  imasring  14043  opprrng  14056  opprrngbg  14057  opprring  14058  mulgass3  14064  dvdsrd  14074  dvdsrneg  14083  unitnegcl  14110  dvrvald  14114  dvrid  14117  dvr1  14118  dvrass  14119  dvrdir  14123  ringinvdv  14125  rhmex  14137  isrim0  14141  rhmval  14153  rhmdvdsr  14155  rhmopp  14156  elrhmunit  14157  rhmunitinv  14158  isnzr2  14164  ringelnzr  14167  issubrng2  14190  issubrg2  14221  aprap  14266  lmodvs1  14296  lmod0vs  14301  lmodvs0  14302  lmodvsmmulgdi  14303  lmodfopne  14306  lmodvneg1  14310  lss1  14342  islss3  14359  lsslss  14361  lss1d  14363  lspf  14369  lspsn  14396  lspsnneg  14400  sraval  14417  sraring  14429  qus1  14506  qusrhm  14508  cnfldui  14569  dvdsrzring  14583  mulgghm2  14588  mulgrhm  14589  znval  14616  znf1o  14631  psrbagfi  14653  psrplusgg  14658  mplgrpfi  14686  eltg2b  14744  difopn  14798  ntrcls0  14821  neii1  14837  restbasg  14858  resttopon  14861  restuni2  14867  cnrest2r  14927  tx1cn  14959  txcnp  14961  txcn  14965  txswaphmeo  15011  psmettri  15020  xmeteq0  15049  xmettri  15062  metrtri  15067  ssblex  15121  xmeter  15126  isxms2  15142  cnbl0  15224  cnblcld  15225  reopnap  15236  tgioo  15244  addcncntoplem  15251  expcn  15259  rescncf  15271  cncfcdm  15272  mulc1cncf  15279  cncfcncntop  15283  addccncf  15290  cdivcncfap  15294  negcncf  15295  cnopnap  15301  suplociccex  15315  hoverlt1  15339  hovergt0  15340  dich0  15342  limccl  15349  ellimc3apf  15350  cnplimcim  15357  limccnp2lem  15366  reldvg  15369  dvbsssg  15376  dvcjbr  15398  dvcj  15399  dvfre  15400  dvrecap  15403  dvef  15417  plyaddcl  15444  plymulcl  15445  plysubcl  15446  plyrecj  15453  reeff1olem  15461  pilem3  15473  ptolemy  15514  rplogcl  15569  rpcxpef  15584  cxprec  15600  rpcxproot  15604  rplogb1  15638  logbgt0b  15656  logbgcd1irr  15657  binom4  15669  wilthlem1  15670  sgmnncl  15678  dvdsppwf1o  15679  mersenne  15687  lgslem4  15698  lgsval  15699  lgsval2lem  15705  lgsval4a  15717  lgsdir2lem3  15725  lgsdir2  15728  lgsne0  15733  lgsprme0  15737  lgsmulsqcoprm  15741  gausslemma2dlem0a  15744  gausslemma2dlem1a  15753  2lgslem1b  15784  2lgslem2  15787  2lgsoddprm  15808  struct2slots2dom  15855  structvtxval  15856  structiedg0val  15857  struct2griedg  15863  edgstruct  15880  uhgr0vb  15900  incistruhgr  15906  umgrvad2edg  16025  uspgredg2vlem  16034  uspgredg2v  16035  usgredg2v  16038  ushgredgedg  16040  ushgredgedgloop  16042  vtxdgfval  16048  wksfval  16068  wlkpropg  16070  uspgr2wlkeq2  16112  uspgr2wlkeqi  16113  upgr2wlkdc  16121  clwwlkccatlem  16143  clwwlkng  16148  clwwlkext2edg  16164  clwwlknccat  16165  umgr2cwwkdifex  16167  bj-nnan  16183  bj-indind  16378  bj-omtrans  16402  bj-inf2vnlem1  16416  sscoll2  16434  2omap  16446  pw1map  16448  pwtrufal  16450  sssneq  16455  pw1nct  16456  nninfsellemsuc  16466  nninfomnilem  16472  nnnninfex  16476  exmidsbthrlem  16478  qdencn  16483  trilpo  16499  trirec0  16500  apdiff  16504  iswomninnlem  16505  iswomni0  16507  redcwlpo  16511  redc0  16513  reap0  16514  cndcap  16515  dceqnconst  16516  dcapnconst  16517  neapmkv  16524  neap0mkv  16525