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  696  ioran  753  pm3.14  754  pm4.44  780  ordi  817  pm4.39  823  animorl  824  animorlr  826  pm5.16  829  pm5.54dc  919  intnanr  931  intnanrd  933  dcan  935  dedlema  971  dedlemb  972  pm4.42r  973  prlem2  976  simp1l  1023  simp2l  1025  simp3l  1027  3anandis  1358  xordc1  1404  anxordi  1411  falantru  1414  19.26  1495  exsimpl  1631  sbequ2  1783  sbcof2  1824  sbequilem  1852  sbequ8  1861  euan  2101  mooran1  2117  eupickbi  2127  2exeu  2137  dimatis  2162  rexim  2591  r19.26  2623  r19.40  2651  rspcime  2875  rr19.28v  2904  elrab3t  2919  eueq3dc  2938  mosubt  2941  reu6  2953  sbc2iegf  3060  sbcralt  3066  sbcrext  3067  rmob  3082  csbiebt  3124  ssab2  3267  difdif  3288  uneqin  3414  indifdir  3419  undif3ss  3424  rexm  3550  eqifdc  3596  ifandc  3599  ifnebibdc  3604  difsn  3759  opprc1  3830  unissel  3868  ssmin  3893  abssexg  4215  undifexmid  4226  pwntru  4232  exmidundif  4239  exmidundifim  4240  opelopabsb  4294  sess1  4372  ordelord  4416  onin  4421  suctr  4456  abnexg  4481  ifexg  4520  ordtriexmidlem  4555  ordtri2or2exmid  4607  ontri2orexmidim  4608  tfi  4618  peano1  4630  peano2  4631  nnpredcl  4659  0nelxp  4691  0nelelxp  4692  brab2a  4716  mosubopt  4728  posng  4735  opabssxp  4737  ideqg  4817  relssres  4984  trin2  5061  dminss  5084  iota4an  5239  iota2  5248  iotam  5250  fun11uni  5328  imadiflem  5337  funimaexg  5342  fneq12  5351  fvelrnb  5608  dffo4  5710  ffnfv  5720  ffvresb  5725  fmptco  5728  fcoconst  5733  fcof1  5830  isotr  5863  isopolem  5869  f1oiso  5873  acexmidlemcase  5917  ovprc1  5958  fnoprabg  6023  elovmporab  6123  elovmporab1w  6124  uchoice  6195  op1steq  6237  dmmpog  6267  1stconst  6279  f1o2ndf1  6286  brtpos2  6309  tpostpos  6322  tposf12  6327  smores  6350  tfrlemi1  6390  tfr1onlembfn  6402  tfri1dALT  6409  tfrcllembfn  6415  freceq1  6450  freceq2  6451  frectfr  6458  omv2  6523  omsuc  6530  nnsucelsuc  6549  nntri3  6555  nnaordi  6566  nnmordi  6574  nnm00  6588  ecexr  6597  ertr  6607  swoer  6620  erth  6638  ecelqsdm  6664  iinerm  6666  ecinxp  6669  erovlem  6686  pmresg  6735  resixp  6792  elixpsn  6794  mapsnf1o  6796  dom3  6835  mapdom1g  6908  ssenen  6912  phpelm  6927  finexdc  6963  exmidpweq  6970  nnwetri  6977  fiintim  6992  infidc  7000  ssfii  7040  fiss  7043  dcfi  7047  supubti  7065  supisoex  7075  ordiso2  7101  inl11  7131  omp1eomlem  7160  nnnninf  7192  nninfisol  7199  ctssexmid  7216  ismkvnex  7221  omniwomnimkv  7233  nninfwlpor  7240  nninfwlpoim  7244  en2eleq  7262  en2other2  7263  exmidfodomrlemr  7269  exmidfodomrlemrALT  7270  exmidaclem  7275  djuen  7278  djudoml  7286  netap  7321  2omotaplemst  7325  exmidapne  7327  cc1  7332  dmaddpqlem  7444  distrnqg  7454  ltanqi  7469  ltmnqi  7470  ltaddnq  7474  ltrnqg  7487  ltnnnq  7490  enq0sym  7499  addnq0mo  7514  mulnq0mo  7515  addnnnq0  7516  distrnq0  7526  prarloclemn  7566  prarloc  7570  ltdfpr  7573  genplt2i  7577  addnqprl  7596  addnqpru  7597  nqprl  7618  appdivnq  7630  1idprl  7657  1idpru  7658  ltexpri  7680  recexpr  7705  cauappcvgprlemdisj  7718  archrecpr  7731  addsrmo  7810  mulsrmo  7811  addsrpr  7812  mulsrpr  7813  0idsr  7834  1idsr  7835  archsr  7849  prsradd  7853  prsrlt  7854  caucvgsr  7869  map2psrprg  7872  elrealeu  7896  muladd11r  8182  negeu  8217  pncan  8232  pncan3  8234  negsub  8274  addid0  8399  posdif  8482  ltnegcon1  8490  subge0  8502  suble0  8503  lesub0  8506  reapval  8603  reapneg  8624  ap0gt0  8667  aprcl  8673  lt0ap0  8675  recextlem1  8678  recapb  8698  div0ap  8729  recrecap  8736  rec11ap  8737  recgt0  8877  mulgt1  8890  lerec2  8916  recp1lt1  8926  recreclt  8927  ledivp1  8930  negiso  8982  nnsub  9029  avglt1  9230  nnrecl  9247  nnnn0addcl  9279  elnn0nn  9291  nn0ge2m1nn  9309  zaddcl  9366  eluzadd  9630  infregelbex  9672  divfnzn  9695  qaddcl  9709  qreccl  9716  cnref1o  9725  ge0p1rp  9760  divlt1lt  9799  divle1le  9800  addlelt  9843  xrre3  9897  xltnegi  9910  xaddval  9920  xaddcom  9936  xnegdi  9943  xposdif  9957  ixxssixx  9977  iccshftr  10069  iccshftl  10071  iccdil  10073  icccntr  10075  zltaddlt1le  10082  elfz2  10090  peano2fzr  10112  fzdcel  10115  fzsplit2  10125  fzaddel  10134  fzrev2  10160  fzrev2i  10161  fzrev3  10162  elfz1b  10165  fseq1p1m1  10169  uzsubfz0  10204  fzosubel3  10272  eluzgtdifelfzo  10273  fzofzp1b  10304  elfzomelpfzo  10307  exfzdc  10316  fvinim0ffz  10317  zsupcllemex  10320  infssuzcldc  10325  exbtwnzlemshrink  10338  qbtwnz  10341  qbtwnxr  10347  ico0  10351  elicore  10356  xqltnle  10357  apbtwnz  10364  flqge  10372  flqlt  10373  flqltnz  10377  flqbi2  10381  flqaddz  10387  flqmulnn0  10389  intfracq  10412  flqdiv  10413  q0mod  10447  q1mod  10448  mulp1mod1  10457  q2txmodxeq0  10476  modfzo0difsn  10487  frec2uzuzd  10494  frec2uzltd  10495  frec2uzrand  10497  uzennn  10528  seqfveq2g  10569  seq3split  10580  seqsplitg  10581  seq3caopr  10587  seqcaoprg  10588  seqf1oglem2  10612  seqf1og  10613  exp3vallem  10632  exp3val  10633  expnnval  10634  exp1  10637  expcl2lemap  10643  rpexpcl  10650  expnegzap  10665  mulexp  10670  mulexpzap  10671  leexp2r  10685  leexp1a  10686  sq11  10704  subsq  10738  binom2  10743  binom3  10749  zesq  10750  bernneq  10752  sq11ap  10799  zzlesq  10800  mulsubdivbinom2ap  10803  apexp1  10810  facwordi  10832  facubnd  10837  facavg  10838  bcval  10841  bcval5  10855  hashennn  10872  fihashf1rn  10880  fseq1hash  10893  hashdifsn  10911  hashdifpr  10912  hashxp  10918  fiubz  10921  fiubnn  10922  fnfz0hash  10924  ffzo0hash  10926  wrdval  10938  wrdsymb0  10967  shftfvalg  10983  ovshftex  10984  shftdm  10987  shftfib  10988  shftval  10990  shftf  10995  crre  11022  cjexp  11058  cjreim2  11069  uzin2  11152  rexuz3  11155  resqrexlemgt0  11185  resqrex  11191  sqrtgt0  11199  sqrtsq  11209  sqrtmsq  11210  absrpclap  11226  absext  11228  absmul  11234  absid  11236  absexp  11244  nn0abscl  11250  abslt  11253  absle  11254  recvalap  11262  abstri  11269  caubnd2  11282  qdenre  11367  maxabsle  11369  maxabslemval  11373  maxcl  11375  rexanre  11385  min1inf  11397  minabs  11401  minclpr  11402  mul0inf  11406  mingeb  11407  xrmaxiflemcl  11410  xrnegiso  11427  climconst2  11456  climmpt  11465  climres  11468  climcaucn  11516  sumeq1  11520  summodclem2a  11546  isumz  11554  fisumss  11557  fsumzcl2  11570  sumsnf  11574  isumclim3  11588  fsum2dlemstep  11599  fisumcom2  11603  fsumconst  11619  cvgcmpub  11641  binom  11649  binom1p  11650  binom1dif  11652  bcxmas  11654  divcnv  11662  geo2lim  11681  geoisum  11682  geoisumr  11683  geoisum1  11684  mertenslemi1  11700  mertensabs  11702  prod1dc  11751  fprodconst  11785  fprodcom2fi  11791  efcllem  11824  efcj  11838  efadd  11840  efexp  11847  efgt1p2  11860  tanvalap  11873  tanval2ap  11878  tanval3ap  11879  sinadd  11901  cosadd  11902  dvdsdc  11963  iddvdsexp  11980  dvdsadd  12001  dvds1  12018  odd2np1  12038  oddm1even  12040  m1exp1  12066  divalglemnn  12083  fldivndvdslt  12102  flodddiv4lt  12103  bitsp1  12115  dvdsbnd  12123  gcdnncl  12134  zeqzmulgcd  12137  gcdneg  12149  modgcd  12158  bezoutlemex  12168  bezoutlemeu  12174  dfgcd3  12177  gcdzeq  12189  dvdssq  12198  algrf  12213  eucalgval2  12221  eucalgcvga  12226  lcmval  12231  gcddvdslcm  12241  lcmneg  12242  coprmgcdb  12256  qredeu  12265  divgcdcoprm0  12269  divgcdcoprmex  12270  cncongr1  12271  cncongr2  12272  cncongrcoprm  12274  prmind2  12288  dvdsnprmd  12293  exprmfct  12306  isprm6  12315  pw2dvdslemn  12333  oddpwdclemdc  12341  sqrt2irraplemnn  12347  divnumden  12364  divdenle  12365  nn0sqrtelqelz  12374  phivalfi  12380  crth  12392  eulerth  12401  prmdivdiv  12405  reumodprminv  12422  nnnn0modprm0  12424  nnoddn2prmb  12431  pcval  12465  pcidlem  12492  pcid  12493  pcneg  12494  pc2dvds  12499  pcz  12501  pcprod  12515  prmpwdvds  12524  4sqexercise1  12567  2expltfac  12608  xpct  12613  znnen  12615  ennnfonelemg  12620  ennnfone  12642  ctinfom  12645  ctinf  12647  ssomct  12662  isstruct2im  12688  isstruct2r  12689  setsvalg  12708  setsslnid  12730  ressvalsets  12742  ressex  12743  2strbasg  12797  2stropg  12798  2strbas1g  12800  ressmulrg  12822  ressscag  12860  ressvscag  12861  ressipg  12862  restval  12916  restid2  12919  prdsex  12940  qusex  12968  fnpr2o  12982  xpsfval  12991  xpsval  12995  intopsn  13010  mgmidmo  13015  lidrididd  13025  ismnddef  13059  mndinvmod  13086  ismhm  13093  mhmex  13094  insubm  13117  dfgrp2  13159  grpsubval  13178  grpinvinv  13199  grpsubrcan  13213  grpsubadd  13220  grpaddsubass  13222  grpsubsub4  13225  grppnpcan2  13226  grpnpncan  13227  grpnpncan0  13228  grpnnncan2  13229  dfgrp3m  13231  dfgrp3me  13232  imasgrp2  13240  mhmmnd  13246  mulgfvalg  13251  mulgval  13252  mulgfng  13254  mulg1  13259  mulgnnp1  13260  mulgnndir  13281  mulgass  13289  mulgmodid  13291  issubg2m  13319  grpissubg  13324  isnsg  13332  isnsg3  13337  0nsg  13344  eqgfval  13352  eqger  13354  eqgen  13357  eqgcpbl  13358  quseccl  13363  isghm  13373  kerf1ghm  13404  conjghm  13406  conjsubg  13407  abladdsub  13445  ablpncan3  13447  ablsubsub23  13455  invghm  13459  subgabl  13462  mgpress  13487  rngdi  13496  rnglz  13501  imasrng  13512  srgmulgass  13545  srgrmhm  13550  isring  13556  ringo2times  13584  ringrng  13592  ringlz  13599  imasring  13620  opprrng  13633  opprrngbg  13634  opprring  13635  mulgass3  13641  dvdsrd  13650  dvdsrneg  13659  unitnegcl  13686  dvrvald  13690  dvrid  13693  dvr1  13694  dvrass  13695  dvrdir  13699  ringinvdv  13701  rhmex  13713  isrim0  13717  rhmval  13729  rhmdvdsr  13731  rhmopp  13732  elrhmunit  13733  rhmunitinv  13734  isnzr2  13740  ringelnzr  13743  issubrng2  13766  issubrg2  13797  aprap  13842  lmodvs1  13872  lmod0vs  13877  lmodvs0  13878  lmodvsmmulgdi  13879  lmodfopne  13882  lmodvneg1  13886  lss1  13918  islss3  13935  lsslss  13937  lss1d  13939  lspf  13945  lspsn  13972  lspsnneg  13976  sraval  13993  sraring  14005  qus1  14082  qusrhm  14084  cnfldui  14145  dvdsrzring  14159  mulgghm2  14164  mulgrhm  14165  znval  14192  znf1o  14207  psrplusgg  14230  eltg2b  14290  difopn  14344  ntrcls0  14367  neii1  14383  restbasg  14404  resttopon  14407  restuni2  14413  cnrest2r  14473  tx1cn  14505  txcnp  14507  txcn  14511  txswaphmeo  14557  psmettri  14566  xmeteq0  14595  xmettri  14608  metrtri  14613  ssblex  14667  xmeter  14672  isxms2  14688  cnbl0  14770  cnblcld  14771  reopnap  14782  tgioo  14790  addcncntoplem  14797  expcn  14805  rescncf  14817  cncfcdm  14818  mulc1cncf  14825  cncfcncntop  14829  addccncf  14836  cdivcncfap  14840  negcncf  14841  cnopnap  14847  suplociccex  14861  hoverlt1  14885  hovergt0  14886  dich0  14888  limccl  14895  ellimc3apf  14896  cnplimcim  14903  limccnp2lem  14912  reldvg  14915  dvbsssg  14922  dvcjbr  14944  dvcj  14945  dvfre  14946  dvrecap  14949  dvef  14963  plyaddcl  14990  plymulcl  14991  plysubcl  14992  plyrecj  14999  reeff1olem  15007  pilem3  15019  ptolemy  15060  rplogcl  15115  rpcxpef  15130  cxprec  15146  rpcxproot  15150  rplogb1  15184  logbgt0b  15202  logbgcd1irr  15203  binom4  15215  wilthlem1  15216  sgmnncl  15224  dvdsppwf1o  15225  mersenne  15233  lgslem4  15244  lgsval  15245  lgsval2lem  15251  lgsval4a  15263  lgsdir2lem3  15271  lgsdir2  15274  lgsne0  15279  lgsprme0  15283  lgsmulsqcoprm  15287  gausslemma2dlem0a  15290  gausslemma2dlem1a  15299  2lgslem1b  15330  2lgslem2  15333  2lgsoddprm  15354  bj-nnan  15382  bj-indind  15578  bj-omtrans  15602  bj-inf2vnlem1  15616  sscoll2  15634  pwtrufal  15642  sssneq  15646  pw1nct  15647  nninfsellemsuc  15656  nninfomnilem  15662  exmidsbthrlem  15666  qdencn  15671  trilpo  15687  trirec0  15688  apdiff  15692  iswomninnlem  15693  iswomni0  15695  redcwlpo  15699  redc0  15701  reap0  15702  cndcap  15703  dceqnconst  15704  dcapnconst  15705  neapmkv  15712  neap0mkv  15713