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  697  ioran  754  pm3.14  755  pm4.44  781  ordi  818  pm4.39  824  animorl  825  animorlr  827  pm5.16  830  pm5.54dc  920  intnanr  932  intnanrd  934  dcan  936  dedlema  972  dedlemb  973  pm4.42r  974  prlem2  977  simp1l  1024  simp2l  1026  simp3l  1028  3anandis  1360  xordc1  1413  anxordi  1420  falantru  1423  19.26  1504  exsimpl  1640  sbequ2  1792  sbcof2  1833  sbequilem  1861  sbequ8  1870  euan  2110  mooran1  2126  eupickbi  2136  2exeu  2146  dimatis  2171  rexim  2600  r19.26  2632  r19.40  2660  rspcime  2884  rr19.28v  2913  elrab3t  2928  eueq3dc  2947  mosubt  2950  reu6  2962  sbc2iegf  3069  sbcralt  3075  sbcrext  3076  rmob  3091  csbiebt  3133  ssab2  3277  difdif  3298  uneqin  3424  indifdir  3429  undif3ss  3434  rexm  3560  eqifdc  3607  ifandc  3610  ifnebibdc  3615  difsn  3770  opprc1  3841  unissel  3879  ssmin  3904  abssexg  4227  undifexmid  4238  pwntru  4244  exmidundif  4251  exmidundifim  4252  opelopabsb  4307  sess1  4385  ordelord  4429  onin  4434  suctr  4469  abnexg  4494  ifexg  4533  ordtriexmidlem  4568  ordtri2or2exmid  4620  ontri2orexmidim  4621  tfi  4631  peano1  4643  peano2  4644  nnpredcl  4672  0nelxp  4704  0nelelxp  4705  brab2a  4729  mosubopt  4741  posng  4748  opabssxp  4750  ideqg  4830  relssres  4998  trin2  5075  dminss  5098  iota4an  5253  iota2  5262  iotam  5264  fununfun  5318  fun11uni  5345  imadiflem  5354  funimaexg  5359  fneq12  5368  fvelrnb  5628  dffo4  5730  ffnfv  5740  ffvresb  5745  fmptco  5748  fcoconst  5753  funopsn  5764  fcof1  5854  isotr  5887  isopolem  5893  f1oiso  5897  acexmidlemcase  5941  ovprc1  5983  fnoprabg  6048  elovmporab  6148  elovmporab1w  6149  uchoice  6225  op1steq  6267  dmmpog  6297  1stconst  6309  f1o2ndf1  6316  brtpos2  6339  tpostpos  6352  tposf12  6357  smores  6380  tfrlemi1  6420  tfr1onlembfn  6432  tfri1dALT  6439  tfrcllembfn  6445  freceq1  6480  freceq2  6481  frectfr  6488  omv2  6553  omsuc  6560  nnsucelsuc  6579  nntri3  6585  nnaordi  6596  nnmordi  6604  nnm00  6618  ecexr  6627  ertr  6637  swoer  6650  erth  6668  ecelqsdm  6694  iinerm  6696  ecinxp  6699  erovlem  6716  pmresg  6765  resixp  6822  elixpsn  6824  mapsnf1o  6826  dom3  6869  mapdom1g  6946  ssenen  6950  phpelm  6965  finexdc  7001  exmidpweq  7008  nnwetri  7015  fiintim  7030  infidc  7038  ssfii  7078  fiss  7081  dcfi  7085  supubti  7103  supisoex  7113  ordiso2  7139  inl11  7169  omp1eomlem  7198  nnnninf  7230  nninfisol  7237  ctssexmid  7254  ismkvnex  7259  omniwomnimkv  7271  nninfwlpor  7278  nninfwlpoim  7283  nninfinfwlpo  7284  en2eleq  7305  en2other2  7306  exmidfodomrlemr  7312  exmidfodomrlemrALT  7313  acnrcl  7315  exmidaclem  7322  djuen  7325  djudoml  7333  netap  7368  2omotaplemst  7372  exmidapne  7374  cc1  7379  acnccim  7386  dmaddpqlem  7492  distrnqg  7502  ltanqi  7517  ltmnqi  7518  ltaddnq  7522  ltrnqg  7535  ltnnnq  7538  enq0sym  7547  addnq0mo  7562  mulnq0mo  7563  addnnnq0  7564  distrnq0  7574  prarloclemn  7614  prarloc  7618  ltdfpr  7621  genplt2i  7625  addnqprl  7644  addnqpru  7645  nqprl  7666  appdivnq  7678  1idprl  7705  1idpru  7706  ltexpri  7728  recexpr  7753  cauappcvgprlemdisj  7766  archrecpr  7779  addsrmo  7858  mulsrmo  7859  addsrpr  7860  mulsrpr  7861  0idsr  7882  1idsr  7883  archsr  7897  prsradd  7901  prsrlt  7902  caucvgsr  7917  map2psrprg  7920  elrealeu  7944  muladd11r  8230  negeu  8265  pncan  8280  pncan3  8282  negsub  8322  addid0  8447  posdif  8530  ltnegcon1  8538  subge0  8550  suble0  8551  lesub0  8554  reapval  8651  reapneg  8672  ap0gt0  8715  aprcl  8721  lt0ap0  8723  recextlem1  8726  recapb  8746  div0ap  8777  recrecap  8784  rec11ap  8785  recgt0  8925  mulgt1  8938  lerec2  8964  recp1lt1  8974  recreclt  8975  ledivp1  8978  negiso  9030  nnsub  9077  avglt1  9278  nnrecl  9295  nnnn0addcl  9327  elnn0nn  9339  nn0ge2m1nn  9357  zaddcl  9414  eluzadd  9679  infregelbex  9721  divfnzn  9744  qaddcl  9758  qreccl  9765  cnref1o  9774  ge0p1rp  9809  divlt1lt  9848  divle1le  9849  addlelt  9892  xrre3  9946  xltnegi  9959  xaddval  9969  xaddcom  9985  xnegdi  9992  xposdif  10006  ixxssixx  10026  iccshftr  10118  iccshftl  10120  iccdil  10122  icccntr  10124  zltaddlt1le  10131  elfz2  10139  peano2fzr  10161  fzdcel  10164  fzsplit2  10174  fzaddel  10183  fzrev2  10209  fzrev2i  10210  fzrev3  10211  elfz1b  10214  fseq1p1m1  10218  uzsubfz0  10253  fzosubel3  10327  eluzgtdifelfzo  10328  fzofzp1b  10359  elfzomelpfzo  10362  exfzdc  10371  fvinim0ffz  10372  zsupcllemex  10375  infssuzcldc  10380  exbtwnzlemshrink  10393  qbtwnz  10396  qbtwnxr  10402  ico0  10406  elicore  10411  xqltnle  10412  apbtwnz  10419  flqge  10427  flqlt  10428  flqltnz  10432  flqbi2  10436  flqaddz  10442  flqmulnn0  10444  intfracq  10467  flqdiv  10468  q0mod  10502  q1mod  10503  mulp1mod1  10512  q2txmodxeq0  10531  modfzo0difsn  10542  frec2uzuzd  10549  frec2uzltd  10550  frec2uzrand  10552  uzennn  10583  seqfveq2g  10624  seq3split  10635  seqsplitg  10636  seq3caopr  10642  seqcaoprg  10643  seqf1oglem2  10667  seqf1og  10668  exp3vallem  10687  exp3val  10688  expnnval  10689  exp1  10692  expcl2lemap  10698  rpexpcl  10705  expnegzap  10720  mulexp  10725  mulexpzap  10726  leexp2r  10740  leexp1a  10741  sq11  10759  subsq  10793  binom2  10798  binom3  10804  zesq  10805  bernneq  10807  sq11ap  10854  zzlesq  10855  mulsubdivbinom2ap  10858  apexp1  10865  facwordi  10887  facubnd  10892  facavg  10893  bcval  10896  bcval5  10910  hashennn  10927  fihashf1rn  10935  fseq1hash  10948  hashdifsn  10966  hashdifpr  10967  hashxp  10973  fiubz  10976  fiubnn  10977  fnfz0hash  10979  ffzo0hash  10981  hash2en  10990  wrdval  10999  wrdsymb0  11028  ccatsymb  11061  ccatval21sw  11064  lswccatn0lsw  11070  s111  11088  ccat1st1st  11096  lswccats1fst  11099  swrdlen2  11118  swrdfv2  11119  swrdsbslen  11122  swrds1  11124  ccatswrd  11126  pfxval  11130  pfxclg  11133  pfxmpt  11134  pfxid  11140  pfxfv0  11146  pfxtrcfv0  11148  pfxfvlsw  11149  pfxeq  11150  ccatpfx  11155  shftfvalg  11162  ovshftex  11163  shftdm  11166  shftfib  11167  shftval  11169  shftf  11174  crre  11201  cjexp  11237  cjreim2  11248  uzin2  11331  rexuz3  11334  resqrexlemgt0  11364  resqrex  11370  sqrtgt0  11378  sqrtsq  11388  sqrtmsq  11389  absrpclap  11405  absext  11407  absmul  11413  absid  11415  absexp  11423  nn0abscl  11429  abslt  11432  absle  11433  recvalap  11441  abstri  11448  caubnd2  11461  qdenre  11546  maxabsle  11548  maxabslemval  11552  maxcl  11554  rexanre  11564  min1inf  11576  minabs  11580  minclpr  11581  mul0inf  11585  mingeb  11586  xrmaxiflemcl  11589  xrnegiso  11606  climconst2  11635  climmpt  11644  climres  11647  climcaucn  11695  sumeq1  11699  summodclem2a  11725  isumz  11733  fisumss  11736  fsumzcl2  11749  sumsnf  11753  isumclim3  11767  fsum2dlemstep  11778  fisumcom2  11782  fsumconst  11798  cvgcmpub  11820  binom  11828  binom1p  11829  binom1dif  11831  bcxmas  11833  divcnv  11841  geo2lim  11860  geoisum  11861  geoisumr  11862  geoisum1  11863  mertenslemi1  11879  mertensabs  11881  prod1dc  11930  fprodconst  11964  fprodcom2fi  11970  efcllem  12003  efcj  12017  efadd  12019  efexp  12026  efgt1p2  12039  tanvalap  12052  tanval2ap  12057  tanval3ap  12058  sinadd  12080  cosadd  12081  dvdsdc  12142  iddvdsexp  12159  dvdsadd  12180  dvds1  12197  odd2np1  12217  oddm1even  12219  m1exp1  12245  divalglemnn  12262  fldivndvdslt  12281  flodddiv4lt  12282  bitsp1  12295  bitsmod  12300  bitsfi  12301  bitscmp  12302  bitsinv1lem  12305  dvdsbnd  12310  gcdnncl  12321  zeqzmulgcd  12324  gcdneg  12336  modgcd  12345  bezoutlemex  12355  bezoutlemeu  12361  dfgcd3  12364  gcdzeq  12376  dvdssq  12385  algrf  12400  eucalgval2  12408  eucalgcvga  12413  lcmval  12418  gcddvdslcm  12428  lcmneg  12429  coprmgcdb  12443  qredeu  12452  divgcdcoprm0  12456  divgcdcoprmex  12457  cncongr1  12458  cncongr2  12459  cncongrcoprm  12461  prmind2  12475  dvdsnprmd  12480  exprmfct  12493  isprm6  12502  pw2dvdslemn  12520  oddpwdclemdc  12528  sqrt2irraplemnn  12534  divnumden  12551  divdenle  12552  nn0sqrtelqelz  12561  phivalfi  12567  crth  12579  eulerth  12588  prmdivdiv  12592  reumodprminv  12609  nnnn0modprm0  12611  nnoddn2prmb  12618  pcval  12652  pcidlem  12679  pcid  12680  pcneg  12681  pc2dvds  12686  pcz  12688  pcprod  12702  prmpwdvds  12711  4sqexercise1  12754  2expltfac  12795  xpct  12800  znnen  12802  ennnfonelemg  12807  ennnfone  12829  ctinfom  12832  ctinf  12834  ssomct  12849  isstruct2im  12875  isstruct2r  12876  setsvalg  12895  setsslnid  12917  ressvalsets  12929  ressex  12930  2strbasg  12985  2stropg  12986  2strbas1g  12988  ressmulrg  13010  ressscag  13048  ressvscag  13049  ressipg  13050  restval  13110  restid2  13113  prdsex  13134  pwsval  13156  qusex  13190  fnpr2o  13204  xpsfval  13213  xpsval  13217  intopsn  13232  mgmidmo  13237  lidrididd  13247  ismnddef  13283  mndinvmod  13310  imasmnd2  13317  ismhm  13326  mhmex  13327  insubm  13350  dfgrp2  13392  grpsubval  13411  grpinvinv  13432  grpsubrcan  13446  grpsubadd  13453  grpaddsubass  13455  grpsubsub4  13458  grppnpcan2  13459  grpnpncan  13460  grpnpncan0  13461  grpnnncan2  13462  dfgrp3m  13464  dfgrp3me  13465  imasgrp2  13479  mhmmnd  13485  mulgfvalg  13490  mulgval  13491  mulgfng  13493  mulg1  13498  mulgnnp1  13499  mulgnndir  13520  mulgass  13528  mulgmodid  13530  issubg2m  13558  grpissubg  13563  isnsg  13571  isnsg3  13576  0nsg  13583  eqgfval  13591  eqger  13593  eqgen  13596  eqgcpbl  13597  quseccl  13602  isghm  13612  kerf1ghm  13643  conjghm  13645  conjsubg  13646  abladdsub  13684  ablpncan3  13686  ablsubsub23  13694  invghm  13698  subgabl  13701  mgpress  13726  rngdi  13735  rnglz  13740  imasrng  13751  srgmulgass  13784  srgrmhm  13789  isring  13795  ringo2times  13823  ringrng  13831  ringlz  13838  imasring  13859  opprrng  13872  opprrngbg  13873  opprring  13874  mulgass3  13880  dvdsrd  13889  dvdsrneg  13898  unitnegcl  13925  dvrvald  13929  dvrid  13932  dvr1  13933  dvrass  13934  dvrdir  13938  ringinvdv  13940  rhmex  13952  isrim0  13956  rhmval  13968  rhmdvdsr  13970  rhmopp  13971  elrhmunit  13972  rhmunitinv  13973  isnzr2  13979  ringelnzr  13982  issubrng2  14005  issubrg2  14036  aprap  14081  lmodvs1  14111  lmod0vs  14116  lmodvs0  14117  lmodvsmmulgdi  14118  lmodfopne  14121  lmodvneg1  14125  lss1  14157  islss3  14174  lsslss  14176  lss1d  14178  lspf  14184  lspsn  14211  lspsnneg  14215  sraval  14232  sraring  14244  qus1  14321  qusrhm  14323  cnfldui  14384  dvdsrzring  14398  mulgghm2  14403  mulgrhm  14404  znval  14431  znf1o  14446  psrbagfi  14468  psrplusgg  14473  mplgrpfi  14501  eltg2b  14559  difopn  14613  ntrcls0  14636  neii1  14652  restbasg  14673  resttopon  14676  restuni2  14682  cnrest2r  14742  tx1cn  14774  txcnp  14776  txcn  14780  txswaphmeo  14826  psmettri  14835  xmeteq0  14864  xmettri  14877  metrtri  14882  ssblex  14936  xmeter  14941  isxms2  14957  cnbl0  15039  cnblcld  15040  reopnap  15051  tgioo  15059  addcncntoplem  15066  expcn  15074  rescncf  15086  cncfcdm  15087  mulc1cncf  15094  cncfcncntop  15098  addccncf  15105  cdivcncfap  15109  negcncf  15110  cnopnap  15116  suplociccex  15130  hoverlt1  15154  hovergt0  15155  dich0  15157  limccl  15164  ellimc3apf  15165  cnplimcim  15172  limccnp2lem  15181  reldvg  15184  dvbsssg  15191  dvcjbr  15213  dvcj  15214  dvfre  15215  dvrecap  15218  dvef  15232  plyaddcl  15259  plymulcl  15260  plysubcl  15261  plyrecj  15268  reeff1olem  15276  pilem3  15288  ptolemy  15329  rplogcl  15384  rpcxpef  15399  cxprec  15415  rpcxproot  15419  rplogb1  15453  logbgt0b  15471  logbgcd1irr  15472  binom4  15484  wilthlem1  15485  sgmnncl  15493  dvdsppwf1o  15494  mersenne  15502  lgslem4  15513  lgsval  15514  lgsval2lem  15520  lgsval4a  15532  lgsdir2lem3  15540  lgsdir2  15543  lgsne0  15548  lgsprme0  15552  lgsmulsqcoprm  15556  gausslemma2dlem0a  15559  gausslemma2dlem1a  15568  2lgslem1b  15599  2lgslem2  15602  2lgsoddprm  15623  struct2slots2dom  15668  structvtxval  15669  structiedg0val  15670  struct2griedg  15676  edgstruct  15691  bj-nnan  15709  bj-indind  15905  bj-omtrans  15929  bj-inf2vnlem1  15943  sscoll2  15961  2omap  15969  pwtrufal  15971  sssneq  15976  pw1nct  15977  nninfsellemsuc  15986  nninfomnilem  15992  nnnninfex  15996  exmidsbthrlem  15998  qdencn  16003  trilpo  16019  trirec0  16020  apdiff  16024  iswomninnlem  16025  iswomni0  16027  redcwlpo  16031  redc0  16033  reap0  16034  cndcap  16035  dceqnconst  16036  dcapnconst  16037  neapmkv  16044  neap0mkv  16045