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  7318  supubti  7339  supisoex  7349  ordiso2  7375  inl11  7405  omp1eomlem  7434  nnnninf  7466  nninfisol  7473  ctssexmid  7490  ismkvnex  7495  omniwomnimkv  7507  nninfwlpor  7514  nninfwlpoim  7519  nninfinfwlpo  7520  en2eleq  7547  en2other2  7548  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  acnrcl  7557  exmidaclem  7564  djuen  7567  djudoml  7575  netap  7620  2omotaplemst  7624  exmidapne  7626  cc1  7631  acnccim  7638  dmaddpqlem  7744  distrnqg  7754  ltanqi  7769  ltmnqi  7770  ltaddnq  7774  ltrnqg  7787  ltnnnq  7790  enq0sym  7799  addnq0mo  7814  mulnq0mo  7815  addnnnq0  7816  distrnq0  7826  prarloclemn  7866  prarloc  7870  ltdfpr  7873  genplt2i  7877  addnqprl  7896  addnqpru  7897  nqprl  7918  appdivnq  7930  1idprl  7957  1idpru  7958  ltexpri  7980  recexpr  8005  cauappcvgprlemdisj  8018  archrecpr  8031  addsrmo  8110  mulsrmo  8111  addsrpr  8112  mulsrpr  8113  0idsr  8134  1idsr  8135  archsr  8149  prsradd  8153  prsrlt  8154  caucvgsr  8169  map2psrprg  8172  elrealeu  8196  muladd11r  8483  negeu  8518  pncan  8533  pncan3  8535  negsub  8575  addid0  8700  addeq0  8704  posdif  8784  ltnegcon1  8792  subge0  8804  suble0  8805  lesub0  8808  reapval  8906  reapneg  8927  ap0gt0  8970  aprcl  8976  lt0ap0  8978  recextlem1  8981  recapb  9003  div0ap  9034  recrecap  9041  rec11ap  9042  recgt0  9182  mulgt1  9195  lerec2  9221  recp1lt1  9231  recreclt  9232  ledivp1  9235  negiso  9287  nnsub  9345  avglt1  9548  nnrecl  9565  nnnn0addcl  9597  elnn0nn  9609  fcdmnn0fsuppg  9622  nn0ge2m1nn  9631  zaddcl  9688  eluzmn  9937  eluzadd  9960  infregelbex  10007  divfnzn  10030  qaddcl  10044  qreccl  10051  cnref1o  10061  ge0p1rp  10096  divlt1lt  10135  divle1le  10136  addlelt  10179  xrre3  10234  xltnegi  10247  xaddval  10257  xaddcom  10273  xnegdi  10280  xposdif  10294  ixxssixx  10314  iccshftr  10406  iccshftl  10408  iccdil  10410  icccntr  10412  zltaddlt1le  10420  elfz2  10428  peano2fzr  10451  fzdcel  10454  fzsplit2  10465  fzaddel  10475  fzrev2  10502  fzrev2i  10503  fzrev3  10504  elfz1b  10507  fseq1p1m1  10511  uzsubfz0  10546  fzosubel3  10624  eluzgtdifelfzo  10625  fzofzp1b  10656  elfzomelpfzo  10659  exfzdc  10669  fvinim0ffz  10670  zsupcllemex  10673  infssuzcldc  10678  exbtwnzlemshrink  10693  qbtwnz  10696  qbtwnxr  10702  ico0  10706  elicore  10711  xqltnle  10712  apbtwnz  10719  flaplelt  10723  flqge  10729  flapge  10730  flqlt  10731  flqltnz  10735  flqbi2  10739  flqaddz  10745  flqmulnn0  10747  intfracq  10770  flqdiv  10771  q0mod  10805  q1mod  10806  mulp1mod1  10815  q2txmodxeq0  10834  modfzo0difsn  10845  frec2uzuzd  10852  frec2uzltd  10853  frec2uzrand  10855  uzennn  10886  seqfveq2g  10927  seq3split  10938  seqsplitg  10939  seq3caopr  10945  seqcaoprg  10946  seqf1oglem2  10970  seqf1og  10971  exp3vallem  10990  exp3val  10991  expnnval  10992  exp1  10995  expcl2lemap  11001  rpexpcl  11008  expnegzap  11023  mulexp  11028  mulexpzap  11029  leexp2r  11043  leexp1a  11044  sq11  11062  subsq  11096  binom2  11101  binom3  11107  zesq  11109  bernneq  11111  sq11ap  11158  zzlesq  11159  mulsubdivbinom2ap  11163  apexp1  11170  facwordi  11192  facubnd  11197  facavg  11198  bcval  11201  bcval5  11215  hashennn  11233  fihashf1rn  11241  fseq1hash  11255  hashdifsn  11274  hashdifpr  11275  hashxp  11281  hashmap  11282  fiubz  11286  fiubnn  11287  fnfz0hash  11289  ffzo0hash  11291  ssenneg  11294  hashfibclem  11296  hashf1  11301  hash2en  11309  wrdval  11321  ffz0iswrdnn0  11345  wrdsymb0  11351  ccatsymb  11384  ccatval21sw  11387  lswccatn0lsw  11393  ccatalpha  11395  ccatrcl1  11396  s111  11413  ccat1st1st  11423  lswccats1fst  11426  swrdlen2  11448  swrdfv2  11449  swrdsbslen  11452  swrds1  11454  ccatswrd  11456  pfxval  11460  pfxclg  11464  pfxmpt  11466  pfxid  11472  pfxfv0  11478  pfxtrcfv0  11480  pfxfvlsw  11481  pfxeq  11482  ccatpfx  11487  swrdpfx  11493  lenrevpfxcctswrd  11498  wrdeqs1cat  11506  cats1un  11507  swrdccatin1  11511  pfxccatin12lem2a  11513  pfxccatin12lem1  11514  pfxccatin12lem3  11518  pfxccatin12  11519  swrdccat  11521  pfxccat3a  11524  swrdccat3blem  11525  swrdccat3b  11526  reuccatpfxs1lem  11532  reuccatpfxs1  11533  s2cl  11571  s2fv0g  11573  shftfvalg  11597  ovshftex  11598  shftdm  11601  shftfib  11602  shftval  11604  shftf  11609  crre  11636  cjexp  11672  cjreim2  11684  uzin2  11767  rexuz3  11770  resqrexlemgt0  11800  resqrex  11806  sqrtgt0  11814  sqrtsq  11824  sqrtmsq  11825  absrpclap  11841  absext  11843  absmul  11849  absid  11851  qabscl  11857  absexp  11860  nn0abscl  11866  abslt  11869  absle  11870  recvalap  11878  abstri  11885  caubnd2  11898  qdenre  11983  maxabsle  11985  maxabslemval  11989  maxcl  11991  rexanre  12001  min1inf  12013  minabs  12017  minclpr  12018  mul0inf  12023  mingeb  12024  xrmaxiflemcl  12027  xrnegiso  12044  climconst2  12073  climmpt  12082  climres  12085  climcaucn  12133  sumeq1  12137  summodclem2a  12164  isumz  12172  fisumss  12175  fsumzcl2  12188  sumsnf  12192  isumclim3  12206  fsum2dlemstep  12217  fisumcom2  12221  fsumconst  12237  cvgcmpub  12259  binom  12267  binom1p  12268  binom1dif  12270  bcxmas  12272  divcnv  12280  geo2lim  12299  geoisum  12300  geoisumr  12301  geoisum1  12302  mertenslemi1  12318  mertensabs  12320  prod1dc  12369  fprodconst  12403  fprodcom2fi  12409  efcllem  12442  efcj  12456  efadd  12458  efexp  12465  efgt1p2  12478  tanvalap  12491  tanval2ap  12496  tanval3ap  12497  sinadd  12519  cosadd  12520  dvdsdc  12581  iddvdsexp  12598  dvdsadd  12619  dvds1  12636  odd2np1  12656  oddm1even  12658  m1exp1  12684  divalglemnn  12701  fldivndvdslt  12720  flodddiv4lt  12721  bitsp1  12734  bitsmod  12739  bitsfi  12740  bitscmp  12741  bitsinv1lem  12744  dvdsbnd  12749  gcdnncl  12760  zeqzmulgcd  12763  gcdneg  12775  modgcd  12784  bezoutlemex  12794  bezoutlemeu  12800  dfgcd3  12803  gcdzeq  12815  dvdssq  12824  algrf  12839  eucalgval2  12847  eucalgcvga  12852  lcmval  12857  gcddvdslcm  12867  lcmneg  12868  coprmgcdb  12882  qredeu  12891  divgcdcoprm0  12895  divgcdcoprmex  12896  cncongr1  12897  cncongr2  12898  cncongrcoprm  12900  prmind2  12914  dvdsnprmd  12919  exprmfct  12933  isprm6  12942  pwbdvds  12961  nnmaxpwlemnfac  12967  nnmaxpwlemparts  12968  nnmaxpw  12969  sqrt2irraplemnn  12975  divnumden  12992  divdenle  12993  nn0sqrtelqelz  13002  phivalfi  13010  crth  13022  eulerth  13031  prmdivdiv  13035  reumodprminv  13052  nnnn0modprm0  13054  nnoddn2prmb  13061  pcval  13095  pcidlem  13122  pcid  13123  pcneg  13124  pc2dvds  13129  pcz  13131  pcprod  13145  prmpwdvds  13154  4sqexercise1  13197  2expltfac  13239  prmlem0  13240  ballotfilemfval  13278  ballotfilemefi  13286  ballotfilemodife  13289  ballotfilem4  13290  ballotfilemsval  13301  ballotfilemieq  13309  ballotfilemrv  13312  ballotfilemrinv0  13325  xpct  13336  znnen  13338  ennnfonelemg  13343  ennnfone  13365  ctinfom  13368  ctinf  13370  ssomct  13385  isstruct2im  13411  isstruct2r  13412  setsvalg  13431  setsslnid  13453  ressvalsets  13467  ressex  13468  2strbasg  13523  2stropg  13524  2strbas1g  13526  ressmulrg  13548  ressscag  13586  ressvscag  13587  ressipg  13588  restval  13648  restid2  13651  qusex  13695  fnpr2o  13709  xpsfval  13718  intopsn  13736  mgmidmo  13741  lidrididd  13751  ismnddef  13780  mndinvmod  13807  imasmnd2  13808  ismhm  13817  mhmex  13818  insubm  13841  dfgrp2  13881  grpsubval  13900  grpinvinv  13921  grpsubrcan  13935  grpsubadd  13942  grpaddsubass  13944  grpsubsub4  13947  grppnpcan2  13948  grpnpncan  13949  grpnpncan0  13950  grpnnncan2  13951  dfgrp3m  13953  dfgrp3me  13954  imasgrp2  13962  mhmmnd  13968  mulgfvalg  13973  mulgval  13974  mulgfng  13976  mulg1  13981  mulgnnp1  13982  mulgnndir  14003  mulgass  14011  mulgmodid  14013  issubg2m  14041  grpissubg  14046  isnsg  14054  isnsg3  14059  0nsg  14066  eqgfval  14074  eqger  14076  eqgen  14079  eqgcpbl  14080  quseccl  14085  isghm  14095  kerf1ghm  14126  conjghm  14128  conjsubg  14129  abladdsub  14168  ablpncan3  14170  ablsubsub23  14178  invghm  14182  subgabl  14185  prdsex  14221  xpsval  14250  pwsval  14253  mgpress  14279  rngdi  14288  rnglz  14293  imasrng  14304  srgmulgass  14342  srgrmhm  14347  isring  14353  ringo2times  14382  ringrng  14390  ringlz  14397  imasring  14418  opprrng  14431  opprrngbg  14432  opprring  14433  mulgass3  14440  dvdsrd  14450  dvdsrneg  14459  unitnegcl  14486  dvrvald  14490  dvrid  14493  dvr1  14494  dvrass  14495  dvrdir  14499  ringinvdv  14501  rhmex  14513  isrim0  14517  rhmval  14529  rhmdvdsr  14531  rhmopp  14532  elrhmunit  14533  rhmunitinv  14534  isnzr2  14540  ringelnzr  14543  issubrng2  14567  issubrg2  14598  ringunitap  14642  aprap  14647  aprnzr  14648  opprdrng  14669  lmodvs1  14702  lmod0vs  14707  lmodvs0  14708  lmodvsmmulgdi  14709  lmodfopne  14712  lmodvneg1  14716  lss1  14748  islss3  14765  lsslss  14767  lss1d  14769  lspf  14775  lspsn  14802  lspsnneg  14806  sraval  14823  sraring  14835  qus1  14912  qusrhm  14914  cnfldui  14973  dvdsrzring  14987  mulgghm2  14992  mulgrhm  14993  znval  15020  znf1o  15035  assa2ass  15058  assa2ass2  15059  issubassa3  15061  assamulgscmlem2  15091  psrbagfi  15108  psrbagconcl  15112  psrplusgg  15118  mplgrpfi  15146  eltg2b  15204  difopn  15258  ntrcls0  15281  neii1  15297  restbasg  15318  resttopon  15321  restuni2  15327  cnrest2r  15387  tx1cn  15419  txcnp  15421  txcn  15425  txswaphmeo  15471  psmettri  15480  xmeteq0  15509  xmettri  15522  metrtri  15527  ssblex  15581  xmeter  15586  isxms2  15602  cnbl0  15684  cnblcld  15685  reopnap  15696  tgioo  15704  addcncntoplem  15711  expcn  15719  rescncf  15731  cncfcdm  15732  mulc1cncf  15739  cncfcncntop  15743  addccncf  15750  cdivcncfap  15754  negcncf  15755  cnopnap  15761  suplociccex  15775  hoverlt1  15799  hovergt0  15800  dich0  15802  limccl  15809  ellimc3apf  15810  cnplimcim  15817  limccnp2lem  15826  reldvg  15829  dvbsssg  15836  dvcjbr  15858  dvcj  15859  dvfre  15860  dvrecap  15863  dvef  15877  plyaddcl  15904  plymulcl  15905  plysubcl  15906  plyrecj  15913  reeff1olem  15921  pilem3  15934  ptolemy  15975  rplogcl  16031  rpcxpef  16049  cxprec  16065  rpcxproot  16069  rplogb1  16103  logbgt0b  16121  logbgcd1irr  16122  zprmlogbaplem3  16136  binom4  16138  birthdaylem1g  16144  wilthlem1  16151  sgmnncl  16169  ppiprm  16170  dvdsppwf1o  16184  ppiublem1  16192  ppiqub  16194  mersenne  16195  lgslem4  16220  lgsval  16221  lgsval2lem  16227  lgsval4a  16239  lgsdir2lem3  16247  lgsdir2  16250  lgsne0  16255  lgsprme0  16259  lgsmulsqcoprm  16263  gausslemma2dlem0a  16266  gausslemma2dlem1a  16275  2lgslem1b  16306  2lgslem2  16309  2lgsoddprm  16330  struct2slots2dom  16377  structvtxval  16378  structiedg0val  16379  struct2griedg  16385  edgstruct  16403  uhgr0vb  16423  incistruhgr  16429  umgrvad2edg  16550  uspgredg2vlem  16559  uspgredg2v  16560  usgredg2v  16563  ushgredgedg  16565  ushgredgedgloop  16567  usgr0vb  16572  uhgr0vusgr  16577  edg0usgr  16586  subupgr  16612  upgrspanop  16622  umgrspanop  16623  usgrspanop  16624  vtxdgfval  16627  wksfval  16661  wlkpropg  16663  uspgr2wlkeq2  16705  uspgr2wlkeqi  16706  upgr2wlkdc  16716  trlsex  16726  clwwlkccatlem  16739  clwwlkng  16744  clwwlkext2edg  16761  clwwlknccat  16762  umgr2cwwkdifex  16764  clwwlknonel  16771  clwwlknonccat  16772  clwwlknonex2lem2  16777  clwwlknun  16780  eupthsg  16784  eupth2lem3lem6fi  16810  dichmul0orlem7  16857  dichmul0or  16858  bj-nnan  16862  bj-indind  17056  bj-omtrans  17080  bj-inf2vnlem1  17094  sscoll2  17112  pw1map  17123  pwtrufal  17125  sssneq  17130  pw1nct  17131  exmidnotnotr  17134  nninfsellemsuc  17153  nninfomnilem  17159  nnnninfex  17163  exmidsbthrlem  17165  qdencn  17170  trilpo  17190  trirec0  17191  apdiff  17195  iswomninnlem  17197  iswomni0  17199  redcwlpo  17203  redc0  17205  reap0  17206  cndcap  17207  dceqnconst  17208  dcapnconst  17209  neapmkv  17216  neap0mkv  17217  als-no-surprise  17245