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  695  ioran  752  pm3.14  753  pm4.44  779  ordi  816  pm4.39  822  animorl  823  animorlr  825  pm5.16  828  pm5.54dc  918  intnanr  930  intnanrd  932  dcan  933  dedlema  969  dedlemb  970  pm4.42r  971  prlem2  974  simp1l  1021  simp2l  1023  simp3l  1025  3anandis  1347  xordc1  1393  anxordi  1400  falantru  1403  19.26  1481  exsimpl  1617  sbequ2  1769  sbcof2  1810  sbequilem  1838  sbequ8  1847  euan  2082  mooran1  2098  eupickbi  2108  2exeu  2118  dimatis  2143  rexim  2571  r19.26  2603  r19.40  2631  rspcime  2848  rr19.28v  2877  elrab3t  2892  eueq3dc  2911  mosubt  2914  reu6  2926  sbc2iegf  3033  sbcralt  3039  sbcrext  3040  rmob  3055  csbiebt  3096  ssab2  3239  difdif  3260  uneqin  3386  indifdir  3391  undif3ss  3396  rexm  3522  eqifdc  3569  ifandc  3572  difsn  3729  opprc1  3800  unissel  3838  ssmin  3863  abssexg  4181  undifexmid  4192  pwntru  4198  exmidundif  4205  exmidundifim  4206  opelopabsb  4259  sess1  4336  ordelord  4380  onin  4385  suctr  4420  abnexg  4445  ordtriexmidlem  4517  ordtri2or2exmid  4569  ontri2orexmidim  4570  tfi  4580  peano1  4592  peano2  4593  nnpredcl  4621  0nelxp  4653  0nelelxp  4654  brab2a  4678  mosubopt  4690  posng  4697  opabssxp  4699  ideqg  4777  relssres  4944  trin2  5019  dminss  5042  iota4an  5196  iota2  5205  iotam  5207  fun11uni  5285  imadiflem  5294  funimaexg  5299  fneq12  5308  fvelrnb  5562  dffo4  5663  ffnfv  5673  ffvresb  5678  fmptco  5681  fcoconst  5686  fcof1  5781  isotr  5814  isopolem  5820  f1oiso  5824  acexmidlemcase  5867  ovprc1  5908  fnoprabg  5973  op1steq  6177  dmmpog  6207  1stconst  6219  f1o2ndf1  6226  brtpos2  6249  tpostpos  6262  tposf12  6267  smores  6290  tfrlemi1  6330  tfr1onlembfn  6342  tfri1dALT  6349  tfrcllembfn  6355  freceq1  6390  freceq2  6391  frectfr  6398  omv2  6463  omsuc  6470  nnsucelsuc  6489  nntri3  6495  nnaordi  6506  nnmordi  6514  nnm00  6528  ecexr  6537  ertr  6547  swoer  6560  erth  6576  ecelqsdm  6602  iinerm  6604  ecinxp  6607  erovlem  6624  pmresg  6673  resixp  6730  elixpsn  6732  mapsnf1o  6734  dom3  6773  mapdom1g  6844  ssenen  6848  phpelm  6863  finexdc  6899  exmidpweq  6906  nnwetri  6912  fiintim  6925  ssfii  6970  fiss  6973  dcfi  6977  supubti  6995  supisoex  7005  ordiso2  7031  inl11  7061  omp1eomlem  7090  nnnninf  7121  nninfisol  7128  ctssexmid  7145  ismkvnex  7150  omniwomnimkv  7162  nninfwlpor  7169  nninfwlpoim  7173  en2eleq  7191  en2other2  7192  exmidfodomrlemr  7198  exmidfodomrlemrALT  7199  exmidaclem  7204  djuen  7207  djudoml  7215  netap  7250  2omotaplemst  7254  exmidapne  7256  cc1  7261  dmaddpqlem  7373  distrnqg  7383  ltanqi  7398  ltmnqi  7399  ltaddnq  7403  ltrnqg  7416  ltnnnq  7419  enq0sym  7428  addnq0mo  7443  mulnq0mo  7444  addnnnq0  7445  distrnq0  7455  prarloclemn  7495  prarloc  7499  ltdfpr  7502  genplt2i  7506  addnqprl  7525  addnqpru  7526  nqprl  7547  appdivnq  7559  1idprl  7586  1idpru  7587  ltexpri  7609  recexpr  7634  cauappcvgprlemdisj  7647  archrecpr  7660  addsrmo  7739  mulsrmo  7740  addsrpr  7741  mulsrpr  7742  0idsr  7763  1idsr  7764  archsr  7778  prsradd  7782  prsrlt  7783  caucvgsr  7798  map2psrprg  7801  elrealeu  7825  muladd11r  8109  negeu  8144  pncan  8159  pncan3  8161  negsub  8201  addid0  8326  posdif  8408  ltnegcon1  8416  subge0  8428  suble0  8429  lesub0  8432  reapval  8529  reapneg  8550  ap0gt0  8593  aprcl  8599  lt0ap0  8601  recextlem1  8604  recapb  8624  div0ap  8655  recrecap  8662  rec11ap  8663  recgt0  8803  mulgt1  8816  lerec2  8842  recp1lt1  8852  recreclt  8853  ledivp1  8856  negiso  8908  nnsub  8954  avglt1  9153  nnrecl  9170  nnnn0addcl  9202  elnn0nn  9214  nn0ge2m1nn  9232  zaddcl  9289  eluzadd  9552  infregelbex  9594  divfnzn  9617  qaddcl  9631  qreccl  9638  cnref1o  9646  ge0p1rp  9681  divlt1lt  9720  divle1le  9721  addlelt  9764  xrre3  9818  xltnegi  9831  xaddval  9841  xaddcom  9857  xnegdi  9864  xposdif  9878  ixxssixx  9898  iccshftr  9990  iccshftl  9992  iccdil  9994  icccntr  9996  zltaddlt1le  10003  elfz2  10011  peano2fzr  10032  fzdcel  10035  fzsplit2  10045  fzaddel  10054  fzrev2  10080  fzrev2i  10081  fzrev3  10082  elfz1b  10085  fseq1p1m1  10089  uzsubfz0  10124  fzosubel3  10191  eluzgtdifelfzo  10192  fzofzp1b  10223  elfzomelpfzo  10226  exfzdc  10235  fvinim0ffz  10236  exbtwnzlemshrink  10244  qbtwnz  10247  qbtwnxr  10253  ico0  10257  elicore  10262  apbtwnz  10269  flqge  10277  flqlt  10278  flqltnz  10282  flqbi2  10286  flqaddz  10292  flqmulnn0  10294  intfracq  10315  flqdiv  10316  q0mod  10350  q1mod  10351  mulp1mod1  10360  q2txmodxeq0  10379  modfzo0difsn  10390  frec2uzuzd  10397  frec2uzltd  10398  frec2uzrand  10400  uzennn  10431  seq3split  10474  seq3caopr  10478  exp3vallem  10516  exp3val  10517  expnnval  10518  exp1  10521  expcl2lemap  10527  rpexpcl  10534  expnegzap  10549  mulexp  10554  mulexpzap  10555  leexp2r  10569  leexp1a  10570  sq11  10587  subsq  10621  binom2  10626  binom3  10632  zesq  10633  bernneq  10635  sq11ap  10682  apexp1  10691  facwordi  10713  facubnd  10718  facavg  10719  bcval  10722  bcval5  10736  hashennn  10753  fihashf1rn  10761  fseq1hash  10774  hashdifsn  10792  hashdifpr  10793  hashxp  10799  fiubz  10802  fiubnn  10803  fnfz0hash  10805  ffzo0hash  10807  shftfvalg  10820  ovshftex  10821  shftdm  10824  shftfib  10825  shftval  10827  shftf  10832  crre  10859  cjexp  10895  cjreim2  10906  uzin2  10989  rexuz3  10992  resqrexlemgt0  11022  resqrex  11028  sqrtgt0  11036  sqrtsq  11046  sqrtmsq  11047  absrpclap  11063  absext  11065  absmul  11071  absid  11073  absexp  11081  nn0abscl  11087  abslt  11090  absle  11091  recvalap  11099  abstri  11106  caubnd2  11119  qdenre  11204  maxabsle  11206  maxabslemval  11210  maxcl  11212  rexanre  11222  min1inf  11233  minabs  11237  minclpr  11238  mul0inf  11242  mingeb  11243  xrmaxiflemcl  11246  xrnegiso  11263  climconst2  11292  climmpt  11301  climres  11304  climcaucn  11352  sumeq1  11356  summodclem2a  11382  isumz  11390  fisumss  11393  fsumzcl2  11406  sumsnf  11410  isumclim3  11424  fsum2dlemstep  11435  fisumcom2  11439  fsumconst  11455  cvgcmpub  11477  binom  11485  binom1p  11486  binom1dif  11488  bcxmas  11490  divcnv  11498  geo2lim  11517  geoisum  11518  geoisumr  11519  geoisum1  11520  mertenslemi1  11536  mertensabs  11538  prod1dc  11587  fprodconst  11621  fprodcom2fi  11627  efcllem  11660  efcj  11674  efadd  11676  efexp  11683  efgt1p2  11696  tanvalap  11709  tanval2ap  11714  tanval3ap  11715  sinadd  11737  cosadd  11738  dvdsdc  11798  iddvdsexp  11815  dvdsadd  11836  dvds1  11851  odd2np1  11870  oddm1even  11872  m1exp1  11898  divalglemnn  11915  fldivndvdslt  11932  flodddiv4lt  11933  zsupcllemex  11939  infssuzcldc  11944  dvdsbnd  11949  gcdnncl  11960  zeqzmulgcd  11963  gcdneg  11975  modgcd  11984  bezoutlemex  11994  bezoutlemeu  12000  dfgcd3  12003  gcdzeq  12015  dvdssq  12024  algrf  12037  eucalgval2  12045  eucalgcvga  12050  lcmval  12055  gcddvdslcm  12065  lcmneg  12066  coprmgcdb  12080  qredeu  12089  divgcdcoprm0  12093  divgcdcoprmex  12094  cncongr1  12095  cncongr2  12096  cncongrcoprm  12098  prmind2  12112  dvdsnprmd  12117  exprmfct  12130  isprm6  12139  pw2dvdslemn  12157  oddpwdclemdc  12165  sqrt2irraplemnn  12171  divnumden  12188  divdenle  12189  nn0sqrtelqelz  12198  phivalfi  12204  crth  12216  eulerth  12225  prmdivdiv  12229  reumodprminv  12245  nnnn0modprm0  12247  nnoddn2prmb  12254  pcval  12288  pcidlem  12314  pcid  12315  pcneg  12316  pc2dvds  12321  pcz  12323  pcprod  12336  prmpwdvds  12345  xpct  12389  znnen  12391  ennnfonelemg  12396  ennnfone  12418  ctinfom  12421  ctinf  12423  ssomct  12438  isstruct2im  12464  isstruct2r  12465  setsvalg  12484  setsslnid  12506  ressvalsets  12516  ressex  12517  2strbasg  12570  2stropg  12571  2strbas1g  12573  ressmulrg  12595  restval  12682  restid2  12685  intopsn  12718  mgmidmo  12723  lidrididd  12733  ismnddef  12751  mndinvmod  12778  ismhm  12785  insubm  12804  dfgrp2  12834  grpsubval  12851  grpinvinv  12869  grpsubrcan  12883  grpsubadd  12890  grpaddsubass  12892  grpsubsub4  12895  grppnpcan2  12896  grpnpncan  12897  grpnpncan0  12898  grpnnncan2  12899  dfgrp3m  12901  dfgrp3me  12902  mhmmnd  12912  mulgfvalg  12917  mulgval  12918  mulgfng  12919  mulg1  12922  mulgnnp1  12923  mulgnndir  12943  mulgass  12951  mulgmodid  12953  issubg2m  12980  grpissubg  12985  isnsg  12993  isnsg3  12998  0nsg  13005  eqgfval  13012  eqger  13014  eqgen  13017  eqgcpbl  13018  abladdsub  13049  ablpncan3  13051  ablsubsub23  13059  mgpress  13072  srgmulgass  13103  srgrmhm  13108  isring  13114  rngo2times  13142  ringlz  13153  opprring  13180  mulgass3  13185  dvdsrd  13194  dvdsrneg  13203  unitnegcl  13230  dvrvald  13234  dvrid  13237  dvr1  13238  dvrass  13239  dvrdir  13243  ringinvdv  13245  ringelnzr  13259  aprap  13275  issubrg2  13300  dvdsrzring  13362  eltg2b  13425  difopn  13479  ntrcls0  13502  neii1  13518  restbasg  13539  resttopon  13542  restuni2  13548  cnrest2r  13608  tx1cn  13640  txcnp  13642  txcn  13646  txswaphmeo  13692  psmettri  13701  xmeteq0  13730  xmettri  13743  metrtri  13748  ssblex  13802  xmeter  13807  isxms2  13823  cnbl0  13905  cnblcld  13906  reopnap  13909  tgioo  13917  addcncntoplem  13922  rescncf  13939  cncfcdm  13940  mulc1cncf  13947  cncfcncntop  13951  addccncf  13957  cdivcncfap  13958  negcncf  13959  cnopnap  13965  suplociccex  13974  limccl  13999  ellimc3apf  14000  cnplimcim  14007  limccnp2lem  14016  reldvg  14019  dvbsssg  14026  dvcjbr  14043  dvcj  14044  dvfre  14045  dvrecap  14048  dvef  14059  reeff1olem  14063  pilem3  14075  ptolemy  14116  rplogcl  14171  rpcxpef  14186  cxprec  14202  rpcxproot  14205  rplogb1  14237  logbgt0b  14255  logbgcd1irr  14256  binom4  14268  lgslem4  14275  lgsval  14276  lgsval2lem  14282  lgsval4a  14294  lgsdir2lem3  14302  lgsdir2  14305  lgsne0  14310  lgsprme0  14314  lgsmulsqcoprm  14318  bj-nnan  14348  bj-indind  14544  bj-omtrans  14568  bj-inf2vnlem1  14582  sscoll2  14600  pwtrufal  14607  sssneq  14611  pw1nct  14612  nninfsellemsuc  14621  nninfomnilem  14627  exmidsbthrlem  14630  qdencn  14635  trilpo  14651  trirec0  14652  apdiff  14656  iswomninnlem  14657  iswomni0  14659  redcwlpo  14663  redc0  14665  reap0  14666  dceqnconst  14667  dcapnconst  14668  neapmkv  14675  neap0mkv  14676