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  1505  exsimpl  1641  sbequ2  1793  sbcof2  1834  sbequilem  1862  sbequ8  1871  euan  2112  mooran1  2128  eupickbi  2138  2exeu  2148  dimatis  2173  rexim  2602  r19.26  2634  r19.40  2662  rspcime  2891  rr19.28v  2920  elrab3t  2935  eueq3dc  2954  mosubt  2957  reu6  2969  sbc2iegf  3076  sbcralt  3082  sbcrext  3083  rmob  3099  csbiebt  3141  ssab2  3285  difdif  3306  uneqin  3432  indifdir  3437  undif3ss  3442  rexm  3568  eqifdc  3616  ifandc  3620  ifnebibdc  3625  difsn  3781  opprc1  3855  unissel  3893  ssmin  3918  abssexg  4242  undifexmid  4253  pwntru  4259  exmidundif  4266  exmidundifim  4267  opelopabsb  4324  sess1  4402  ordelord  4446  onin  4451  suctr  4486  abnexg  4511  ifexg  4550  ordtriexmidlem  4585  ordtri2or2exmid  4637  ontri2orexmidim  4638  tfi  4648  peano1  4660  peano2  4661  nnpredcl  4689  0nelxp  4721  0nelelxp  4722  brab2a  4746  mosubopt  4758  posng  4765  opabssxp  4767  ideqg  4847  relssres  5016  trin2  5093  dminss  5116  iota4an  5271  iota2  5280  iotam  5282  fununfun  5336  fun11uni  5363  imadiflem  5372  funimaexg  5377  fneq12  5386  fvelrnb  5649  dffo4  5751  ffnfv  5761  ffvresb  5766  fmptco  5769  fcoconst  5774  funopsn  5785  fcof1  5875  isotr  5908  isopolem  5914  f1oiso  5918  acexmidlemcase  5962  ovprc1  6004  fnoprabg  6069  elovmporab  6169  elovmporab1w  6170  uchoice  6246  op1steq  6288  dmmpog  6318  1stconst  6330  f1o2ndf1  6337  brtpos2  6360  tpostpos  6373  tposf12  6378  smores  6401  tfrlemi1  6441  tfr1onlembfn  6453  tfri1dALT  6460  tfrcllembfn  6466  freceq1  6501  freceq2  6502  frectfr  6509  omv2  6574  omsuc  6581  nnsucelsuc  6600  nntri3  6606  nnaordi  6617  nnmordi  6625  nnm00  6639  ecexr  6648  ertr  6658  swoer  6671  erth  6689  ecelqsdm  6715  iinerm  6717  ecinxp  6720  erovlem  6737  pmresg  6786  resixp  6843  elixpsn  6845  mapsnf1o  6847  dom3  6890  mapdom1g  6969  ssenen  6973  phpelm  6989  finexdc  7025  exmidpweq  7032  nnwetri  7039  fiintim  7054  infidc  7062  ssfii  7102  fiss  7105  dcfi  7109  supubti  7127  supisoex  7137  ordiso2  7163  inl11  7193  omp1eomlem  7222  nnnninf  7254  nninfisol  7261  ctssexmid  7278  ismkvnex  7283  omniwomnimkv  7295  nninfwlpor  7302  nninfwlpoim  7307  nninfinfwlpo  7308  en2eleq  7334  en2other2  7335  exmidfodomrlemr  7341  exmidfodomrlemrALT  7342  acnrcl  7344  exmidaclem  7351  djuen  7354  djudoml  7362  netap  7401  2omotaplemst  7405  exmidapne  7407  cc1  7412  acnccim  7419  dmaddpqlem  7525  distrnqg  7535  ltanqi  7550  ltmnqi  7551  ltaddnq  7555  ltrnqg  7568  ltnnnq  7571  enq0sym  7580  addnq0mo  7595  mulnq0mo  7596  addnnnq0  7597  distrnq0  7607  prarloclemn  7647  prarloc  7651  ltdfpr  7654  genplt2i  7658  addnqprl  7677  addnqpru  7678  nqprl  7699  appdivnq  7711  1idprl  7738  1idpru  7739  ltexpri  7761  recexpr  7786  cauappcvgprlemdisj  7799  archrecpr  7812  addsrmo  7891  mulsrmo  7892  addsrpr  7893  mulsrpr  7894  0idsr  7915  1idsr  7916  archsr  7930  prsradd  7934  prsrlt  7935  caucvgsr  7950  map2psrprg  7953  elrealeu  7977  muladd11r  8263  negeu  8298  pncan  8313  pncan3  8315  negsub  8355  addid0  8480  posdif  8563  ltnegcon1  8571  subge0  8583  suble0  8584  lesub0  8587  reapval  8684  reapneg  8705  ap0gt0  8748  aprcl  8754  lt0ap0  8756  recextlem1  8759  recapb  8779  div0ap  8810  recrecap  8817  rec11ap  8818  recgt0  8958  mulgt1  8971  lerec2  8997  recp1lt1  9007  recreclt  9008  ledivp1  9011  negiso  9063  nnsub  9110  avglt1  9311  nnrecl  9328  nnnn0addcl  9360  elnn0nn  9372  nn0ge2m1nn  9390  zaddcl  9447  eluzadd  9712  infregelbex  9754  divfnzn  9777  qaddcl  9791  qreccl  9798  cnref1o  9807  ge0p1rp  9842  divlt1lt  9881  divle1le  9882  addlelt  9925  xrre3  9979  xltnegi  9992  xaddval  10002  xaddcom  10018  xnegdi  10025  xposdif  10039  ixxssixx  10059  iccshftr  10151  iccshftl  10153  iccdil  10155  icccntr  10157  zltaddlt1le  10164  elfz2  10172  peano2fzr  10194  fzdcel  10197  fzsplit2  10207  fzaddel  10216  fzrev2  10242  fzrev2i  10243  fzrev3  10244  elfz1b  10247  fseq1p1m1  10251  uzsubfz0  10286  fzosubel3  10362  eluzgtdifelfzo  10363  fzofzp1b  10394  elfzomelpfzo  10397  exfzdc  10406  fvinim0ffz  10407  zsupcllemex  10410  infssuzcldc  10415  exbtwnzlemshrink  10428  qbtwnz  10431  qbtwnxr  10437  ico0  10441  elicore  10446  xqltnle  10447  apbtwnz  10454  flqge  10462  flqlt  10463  flqltnz  10467  flqbi2  10471  flqaddz  10477  flqmulnn0  10479  intfracq  10502  flqdiv  10503  q0mod  10537  q1mod  10538  mulp1mod1  10547  q2txmodxeq0  10566  modfzo0difsn  10577  frec2uzuzd  10584  frec2uzltd  10585  frec2uzrand  10587  uzennn  10618  seqfveq2g  10659  seq3split  10670  seqsplitg  10671  seq3caopr  10677  seqcaoprg  10678  seqf1oglem2  10702  seqf1og  10703  exp3vallem  10722  exp3val  10723  expnnval  10724  exp1  10727  expcl2lemap  10733  rpexpcl  10740  expnegzap  10755  mulexp  10760  mulexpzap  10761  leexp2r  10775  leexp1a  10776  sq11  10794  subsq  10828  binom2  10833  binom3  10839  zesq  10840  bernneq  10842  sq11ap  10889  zzlesq  10890  mulsubdivbinom2ap  10893  apexp1  10900  facwordi  10922  facubnd  10927  facavg  10928  bcval  10931  bcval5  10945  hashennn  10962  fihashf1rn  10970  fseq1hash  10983  hashdifsn  11001  hashdifpr  11002  hashxp  11008  fiubz  11011  fiubnn  11012  fnfz0hash  11014  ffzo0hash  11016  hash2en  11025  wrdval  11034  wrdsymb0  11063  ccatsymb  11096  ccatval21sw  11099  lswccatn0lsw  11105  s111  11123  ccat1st1st  11131  lswccats1fst  11134  swrdlen2  11153  swrdfv2  11154  swrdsbslen  11157  swrds1  11159  ccatswrd  11161  pfxval  11165  pfxclg  11169  pfxmpt  11171  pfxid  11177  pfxfv0  11183  pfxtrcfv0  11185  pfxfvlsw  11186  pfxeq  11187  ccatpfx  11192  swrdpfx  11198  lenrevpfxcctswrd  11203  wrdeqs1cat  11211  cats1un  11212  swrdccatin1  11216  pfxccatin12lem2a  11218  pfxccatin12lem1  11219  pfxccatin12lem3  11223  pfxccatin12  11224  swrdccat  11226  pfxccat3a  11229  swrdccat3blem  11230  swrdccat3b  11231  reuccatpfxs1lem  11237  reuccatpfxs1  11238  shftfvalg  11244  ovshftex  11245  shftdm  11248  shftfib  11249  shftval  11251  shftf  11256  crre  11283  cjexp  11319  cjreim2  11330  uzin2  11413  rexuz3  11416  resqrexlemgt0  11446  resqrex  11452  sqrtgt0  11460  sqrtsq  11470  sqrtmsq  11471  absrpclap  11487  absext  11489  absmul  11495  absid  11497  absexp  11505  nn0abscl  11511  abslt  11514  absle  11515  recvalap  11523  abstri  11530  caubnd2  11543  qdenre  11628  maxabsle  11630  maxabslemval  11634  maxcl  11636  rexanre  11646  min1inf  11658  minabs  11662  minclpr  11663  mul0inf  11667  mingeb  11668  xrmaxiflemcl  11671  xrnegiso  11688  climconst2  11717  climmpt  11726  climres  11729  climcaucn  11777  sumeq1  11781  summodclem2a  11807  isumz  11815  fisumss  11818  fsumzcl2  11831  sumsnf  11835  isumclim3  11849  fsum2dlemstep  11860  fisumcom2  11864  fsumconst  11880  cvgcmpub  11902  binom  11910  binom1p  11911  binom1dif  11913  bcxmas  11915  divcnv  11923  geo2lim  11942  geoisum  11943  geoisumr  11944  geoisum1  11945  mertenslemi1  11961  mertensabs  11963  prod1dc  12012  fprodconst  12046  fprodcom2fi  12052  efcllem  12085  efcj  12099  efadd  12101  efexp  12108  efgt1p2  12121  tanvalap  12134  tanval2ap  12139  tanval3ap  12140  sinadd  12162  cosadd  12163  dvdsdc  12224  iddvdsexp  12241  dvdsadd  12262  dvds1  12279  odd2np1  12299  oddm1even  12301  m1exp1  12327  divalglemnn  12344  fldivndvdslt  12363  flodddiv4lt  12364  bitsp1  12377  bitsmod  12382  bitsfi  12383  bitscmp  12384  bitsinv1lem  12387  dvdsbnd  12392  gcdnncl  12403  zeqzmulgcd  12406  gcdneg  12418  modgcd  12427  bezoutlemex  12437  bezoutlemeu  12443  dfgcd3  12446  gcdzeq  12458  dvdssq  12467  algrf  12482  eucalgval2  12490  eucalgcvga  12495  lcmval  12500  gcddvdslcm  12510  lcmneg  12511  coprmgcdb  12525  qredeu  12534  divgcdcoprm0  12538  divgcdcoprmex  12539  cncongr1  12540  cncongr2  12541  cncongrcoprm  12543  prmind2  12557  dvdsnprmd  12562  exprmfct  12575  isprm6  12584  pw2dvdslemn  12602  oddpwdclemdc  12610  sqrt2irraplemnn  12616  divnumden  12633  divdenle  12634  nn0sqrtelqelz  12643  phivalfi  12649  crth  12661  eulerth  12670  prmdivdiv  12674  reumodprminv  12691  nnnn0modprm0  12693  nnoddn2prmb  12700  pcval  12734  pcidlem  12761  pcid  12762  pcneg  12763  pc2dvds  12768  pcz  12770  pcprod  12784  prmpwdvds  12793  4sqexercise1  12836  2expltfac  12877  xpct  12882  znnen  12884  ennnfonelemg  12889  ennnfone  12911  ctinfom  12914  ctinf  12916  ssomct  12931  isstruct2im  12957  isstruct2r  12958  setsvalg  12977  setsslnid  12999  ressvalsets  13011  ressex  13012  2strbasg  13067  2stropg  13068  2strbas1g  13070  ressmulrg  13092  ressscag  13130  ressvscag  13131  ressipg  13132  restval  13192  restid2  13195  prdsex  13216  pwsval  13238  qusex  13272  fnpr2o  13286  xpsfval  13295  xpsval  13299  intopsn  13314  mgmidmo  13319  lidrididd  13329  ismnddef  13365  mndinvmod  13392  imasmnd2  13399  ismhm  13408  mhmex  13409  insubm  13432  dfgrp2  13474  grpsubval  13493  grpinvinv  13514  grpsubrcan  13528  grpsubadd  13535  grpaddsubass  13537  grpsubsub4  13540  grppnpcan2  13541  grpnpncan  13542  grpnpncan0  13543  grpnnncan2  13544  dfgrp3m  13546  dfgrp3me  13547  imasgrp2  13561  mhmmnd  13567  mulgfvalg  13572  mulgval  13573  mulgfng  13575  mulg1  13580  mulgnnp1  13581  mulgnndir  13602  mulgass  13610  mulgmodid  13612  issubg2m  13640  grpissubg  13645  isnsg  13653  isnsg3  13658  0nsg  13665  eqgfval  13673  eqger  13675  eqgen  13678  eqgcpbl  13679  quseccl  13684  isghm  13694  kerf1ghm  13725  conjghm  13727  conjsubg  13728  abladdsub  13766  ablpncan3  13768  ablsubsub23  13776  invghm  13780  subgabl  13783  mgpress  13808  rngdi  13817  rnglz  13822  imasrng  13833  srgmulgass  13866  srgrmhm  13871  isring  13877  ringo2times  13905  ringrng  13913  ringlz  13920  imasring  13941  opprrng  13954  opprrngbg  13955  opprring  13956  mulgass3  13962  dvdsrd  13971  dvdsrneg  13980  unitnegcl  14007  dvrvald  14011  dvrid  14014  dvr1  14015  dvrass  14016  dvrdir  14020  ringinvdv  14022  rhmex  14034  isrim0  14038  rhmval  14050  rhmdvdsr  14052  rhmopp  14053  elrhmunit  14054  rhmunitinv  14055  isnzr2  14061  ringelnzr  14064  issubrng2  14087  issubrg2  14118  aprap  14163  lmodvs1  14193  lmod0vs  14198  lmodvs0  14199  lmodvsmmulgdi  14200  lmodfopne  14203  lmodvneg1  14207  lss1  14239  islss3  14256  lsslss  14258  lss1d  14260  lspf  14266  lspsn  14293  lspsnneg  14297  sraval  14314  sraring  14326  qus1  14403  qusrhm  14405  cnfldui  14466  dvdsrzring  14480  mulgghm2  14485  mulgrhm  14486  znval  14513  znf1o  14528  psrbagfi  14550  psrplusgg  14555  mplgrpfi  14583  eltg2b  14641  difopn  14695  ntrcls0  14718  neii1  14734  restbasg  14755  resttopon  14758  restuni2  14764  cnrest2r  14824  tx1cn  14856  txcnp  14858  txcn  14862  txswaphmeo  14908  psmettri  14917  xmeteq0  14946  xmettri  14959  metrtri  14964  ssblex  15018  xmeter  15023  isxms2  15039  cnbl0  15121  cnblcld  15122  reopnap  15133  tgioo  15141  addcncntoplem  15148  expcn  15156  rescncf  15168  cncfcdm  15169  mulc1cncf  15176  cncfcncntop  15180  addccncf  15187  cdivcncfap  15191  negcncf  15192  cnopnap  15198  suplociccex  15212  hoverlt1  15236  hovergt0  15237  dich0  15239  limccl  15246  ellimc3apf  15247  cnplimcim  15254  limccnp2lem  15263  reldvg  15266  dvbsssg  15273  dvcjbr  15295  dvcj  15296  dvfre  15297  dvrecap  15300  dvef  15314  plyaddcl  15341  plymulcl  15342  plysubcl  15343  plyrecj  15350  reeff1olem  15358  pilem3  15370  ptolemy  15411  rplogcl  15466  rpcxpef  15481  cxprec  15497  rpcxproot  15501  rplogb1  15535  logbgt0b  15553  logbgcd1irr  15554  binom4  15566  wilthlem1  15567  sgmnncl  15575  dvdsppwf1o  15576  mersenne  15584  lgslem4  15595  lgsval  15596  lgsval2lem  15602  lgsval4a  15614  lgsdir2lem3  15622  lgsdir2  15625  lgsne0  15630  lgsprme0  15634  lgsmulsqcoprm  15638  gausslemma2dlem0a  15641  gausslemma2dlem1a  15650  2lgslem1b  15681  2lgslem2  15684  2lgsoddprm  15705  struct2slots2dom  15752  structvtxval  15753  structiedg0val  15754  struct2griedg  15760  edgstruct  15775  uhgr0vb  15795  incistruhgr  15801  bj-nnan  15872  bj-indind  16067  bj-omtrans  16091  bj-inf2vnlem1  16105  sscoll2  16123  2omap  16132  pw1map  16134  pwtrufal  16136  sssneq  16141  pw1nct  16142  nninfsellemsuc  16151  nninfomnilem  16157  nnnninfex  16161  exmidsbthrlem  16163  qdencn  16168  trilpo  16184  trirec0  16185  apdiff  16189  iswomninnlem  16190  iswomni0  16192  redcwlpo  16196  redc0  16198  reap0  16199  cndcap  16200  dceqnconst  16201  dcapnconst  16202  neapmkv  16209  neap0mkv  16210