Theorem simpl 108

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 105	1 |- ( ( ph /\ ps ) -> ph )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-ia1 105

This theorem is referenced by:  simpli  110  simpld  111  imp  123  adantrd  277  iba  298  pm3.41  329  pm4.45im  332  anim12  342  pm4.71  387  adantlr  474  adantrr  476  adantllr  478  adantlrr  480  adantrlr  482  adantrrr  484  simplll  528  simplrl  530  simprll  532  simprrl  534  anabs1  567  jcab  598  pm4.38  600  pm5.21  690  ioran  747  pm3.14  748  pm4.44  774  ordi  811  pm4.39  817  animorl  818  animorlr  820  pm5.16  823  pm5.54dc  913  intnanr  925  intnanrd  927  dcan  928  dedlema  964  dedlemb  965  pm4.42r  966  prlem2  969  simp1l  1016  simp2l  1018  simp3l  1020  3anandis  1342  xordc1  1388  anxordi  1395  falantru  1398  19.26  1474  exsimpl  1610  sbequ2  1762  sbcof2  1803  sbequilem  1831  sbequ8  1840  euan  2075  mooran1  2091  eupickbi  2101  2exeu  2111  dimatis  2136  rexim  2564  r19.26  2596  r19.40  2624  rspcime  2841  rr19.28v  2870  elrab3t  2885  eueq3dc  2904  mosubt  2907  reu6  2919  sbc2iegf  3025  sbcralt  3031  sbcrext  3032  rmob  3047  csbiebt  3088  ssab2  3231  difdif  3252  uneqin  3378  indifdir  3383  undif3ss  3388  rexm  3514  eqifdc  3560  ifandc  3563  difsn  3717  opprc1  3787  unissel  3825  ssmin  3850  abssexg  4168  undifexmid  4179  pwntru  4185  exmidundif  4192  exmidundifim  4193  opelopabsb  4245  sess1  4322  ordelord  4366  onin  4371  suctr  4406  abnexg  4431  ordtriexmidlem  4503  ordtri2or2exmid  4555  ontri2orexmidim  4556  tfi  4566  peano1  4578  peano2  4579  nnpredcl  4607  0nelxp  4639  0nelelxp  4640  brab2a  4664  mosubopt  4676  posng  4683  opabssxp  4685  ideqg  4762  relssres  4929  trin2  5002  dminss  5025  iota4an  5179  iota2  5188  iotam  5190  fun11uni  5268  imadiflem  5277  funimaexg  5282  fneq12  5291  fvelrnb  5544  dffo4  5644  ffnfv  5654  ffvresb  5659  fmptco  5662  fcoconst  5667  fcof1  5762  isotr  5795  isopolem  5801  f1oiso  5805  acexmidlemcase  5848  ovprc1  5889  fnoprabg  5954  op1steq  6158  dmmpog  6188  1stconst  6200  f1o2ndf1  6207  brtpos2  6230  tpostpos  6243  tposf12  6248  smores  6271  tfrlemi1  6311  tfr1onlembfn  6323  tfri1dALT  6330  tfrcllembfn  6336  freceq1  6371  freceq2  6372  frectfr  6379  omv2  6444  omsuc  6451  nnsucelsuc  6470  nntri3  6476  nnaordi  6487  nnmordi  6495  nnm00  6509  ecexr  6518  ertr  6528  swoer  6541  erth  6557  ecelqsdm  6583  iinerm  6585  ecinxp  6588  erovlem  6605  pmresg  6654  resixp  6711  elixpsn  6713  mapsnf1o  6715  dom3  6754  mapdom1g  6825  ssenen  6829  phpelm  6844  finexdc  6880  exmidpweq  6887  nnwetri  6893  fiintim  6906  ssfii  6951  fiss  6954  dcfi  6958  supubti  6976  supisoex  6986  ordiso2  7012  inl11  7042  omp1eomlem  7071  nnnninf  7102  nninfisol  7109  ctssexmid  7126  ismkvnex  7131  omniwomnimkv  7143  nninfwlpor  7150  nninfwlpoim  7154  en2eleq  7172  en2other2  7173  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  exmidaclem  7185  djuen  7188  djudoml  7196  cc1  7227  dmaddpqlem  7339  distrnqg  7349  ltanqi  7364  ltmnqi  7365  ltaddnq  7369  ltrnqg  7382  ltnnnq  7385  enq0sym  7394  addnq0mo  7409  mulnq0mo  7410  addnnnq0  7411  distrnq0  7421  prarloclemn  7461  prarloc  7465  ltdfpr  7468  genplt2i  7472  addnqprl  7491  addnqpru  7492  nqprl  7513  appdivnq  7525  1idprl  7552  1idpru  7553  ltexpri  7575  recexpr  7600  cauappcvgprlemdisj  7613  archrecpr  7626  addsrmo  7705  mulsrmo  7706  addsrpr  7707  mulsrpr  7708  0idsr  7729  1idsr  7730  archsr  7744  prsradd  7748  prsrlt  7749  caucvgsr  7764  map2psrprg  7767  elrealeu  7791  muladd11r  8075  negeu  8110  pncan  8125  pncan3  8127  negsub  8167  addid0  8292  posdif  8374  ltnegcon1  8382  subge0  8394  suble0  8395  lesub0  8398  reapval  8495  reapneg  8516  ap0gt0  8559  aprcl  8565  lt0ap0  8567  recextlem1  8569  div0ap  8619  recrecap  8626  rec11ap  8627  recgt0  8766  mulgt1  8779  lerec2  8805  recp1lt1  8815  recreclt  8816  ledivp1  8819  negiso  8871  nnsub  8917  avglt1  9116  nnrecl  9133  nnnn0addcl  9165  elnn0nn  9177  nn0ge2m1nn  9195  zaddcl  9252  eluzadd  9515  infregelbex  9557  divfnzn  9580  qaddcl  9594  qreccl  9601  cnref1o  9609  ge0p1rp  9642  divlt1lt  9681  divle1le  9682  addlelt  9725  xrre3  9779  xltnegi  9792  xaddval  9802  xaddcom  9818  xnegdi  9825  xposdif  9839  ixxssixx  9859  iccshftr  9951  iccshftl  9953  iccdil  9955  icccntr  9957  zltaddlt1le  9964  elfz2  9972  peano2fzr  9993  fzdcel  9996  fzsplit2  10006  fzaddel  10015  fzrev2  10041  fzrev2i  10042  fzrev3  10043  elfz1b  10046  fseq1p1m1  10050  uzsubfz0  10085  fzosubel3  10152  eluzgtdifelfzo  10153  fzofzp1b  10184  elfzomelpfzo  10187  exfzdc  10196  fvinim0ffz  10197  exbtwnzlemshrink  10205  qbtwnz  10208  qbtwnxr  10214  ico0  10218  elicore  10223  apbtwnz  10230  flqge  10238  flqlt  10239  flqltnz  10243  flqbi2  10247  flqaddz  10253  flqmulnn0  10255  intfracq  10276  flqdiv  10277  q0mod  10311  q1mod  10312  mulp1mod1  10321  q2txmodxeq0  10340  modfzo0difsn  10351  frec2uzuzd  10358  frec2uzltd  10359  frec2uzrand  10361  uzennn  10392  seq3split  10435  seq3caopr  10439  exp3vallem  10477  exp3val  10478  expnnval  10479  exp1  10482  expcl2lemap  10488  rpexpcl  10495  expnegzap  10510  mulexp  10515  mulexpzap  10516  leexp2r  10530  leexp1a  10531  sq11  10548  subsq  10582  binom2  10587  binom3  10593  zesq  10594  bernneq  10596  sq11ap  10643  apexp1  10652  facwordi  10674  facubnd  10679  facavg  10680  bcval  10683  bcval5  10697  hashennn  10714  fihashf1rn  10723  fseq1hash  10736  hashdifsn  10754  hashdifpr  10755  hashxp  10761  fiubz  10764  fiubnn  10765  fnfz0hash  10767  ffzo0hash  10769  shftfvalg  10782  ovshftex  10783  shftdm  10786  shftfib  10787  shftval  10789  shftf  10794  crre  10821  cjexp  10857  cjreim2  10868  uzin2  10951  rexuz3  10954  resqrexlemgt0  10984  resqrex  10990  sqrtgt0  10998  sqrtsq  11008  sqrtmsq  11009  absrpclap  11025  absext  11027  absmul  11033  absid  11035  absexp  11043  nn0abscl  11049  abslt  11052  absle  11053  recvalap  11061  abstri  11068  caubnd2  11081  qdenre  11166  maxabsle  11168  maxabslemval  11172  maxcl  11174  rexanre  11184  min1inf  11195  minabs  11199  minclpr  11200  mul0inf  11204  mingeb  11205  xrmaxiflemcl  11208  xrnegiso  11225  climconst2  11254  climmpt  11263  climres  11266  climcaucn  11314  sumeq1  11318  summodclem2a  11344  isumz  11352  fisumss  11355  fsumzcl2  11368  sumsnf  11372  isumclim3  11386  fsum2dlemstep  11397  fisumcom2  11401  fsumconst  11417  cvgcmpub  11439  binom  11447  binom1p  11448  binom1dif  11450  bcxmas  11452  divcnv  11460  geo2lim  11479  geoisum  11480  geoisumr  11481  geoisum1  11482  mertenslemi1  11498  mertensabs  11500  prod1dc  11549  fprodconst  11583  fprodcom2fi  11589  efcllem  11622  efcj  11636  efadd  11638  efexp  11645  efgt1p2  11658  tanvalap  11671  tanval2ap  11676  tanval3ap  11677  sinadd  11699  cosadd  11700  dvdsdc  11760  iddvdsexp  11777  dvdsadd  11798  dvds1  11813  odd2np1  11832  oddm1even  11834  m1exp1  11860  divalglemnn  11877  fldivndvdslt  11894  flodddiv4lt  11895  zsupcllemex  11901  infssuzcldc  11906  dvdsbnd  11911  gcdnncl  11922  zeqzmulgcd  11925  gcdneg  11937  modgcd  11946  bezoutlemex  11956  bezoutlemeu  11962  dfgcd3  11965  gcdzeq  11977  dvdssq  11986  algrf  11999  eucalgval2  12007  eucalgcvga  12012  lcmval  12017  gcddvdslcm  12027  lcmneg  12028  coprmgcdb  12042  qredeu  12051  divgcdcoprm0  12055  divgcdcoprmex  12056  cncongr1  12057  cncongr2  12058  cncongrcoprm  12060  prmind2  12074  dvdsnprmd  12079  exprmfct  12092  isprm6  12101  pw2dvdslemn  12119  oddpwdclemdc  12127  sqrt2irraplemnn  12133  divnumden  12150  divdenle  12151  nn0sqrtelqelz  12160  phivalfi  12166  crth  12178  eulerth  12187  prmdivdiv  12191  reumodprminv  12207  nnnn0modprm0  12209  nnoddn2prmb  12216  pcval  12250  pcidlem  12276  pcid  12277  pcneg  12278  pc2dvds  12283  pcz  12285  pcprod  12298  prmpwdvds  12307  xpct  12351  znnen  12353  ennnfonelemg  12358  ennnfone  12380  ctinfom  12383  ctinf  12385  ssomct  12400  isstruct2im  12426  isstruct2r  12427  setsvalg  12446  setsslnid  12467  ressid2  12477  ressval2  12478  2strbasg  12519  2stropg  12520  2strbas1g  12522  restval  12585  restid2  12588  intopsn  12621  mgmidmo  12626  lidrididd  12636  ismnddef  12654  mndinvmod  12678  ismhm  12685  insubm  12703  dfgrp2  12732  grpsubval  12749  grpinvinv  12766  eltg2b  12848  difopn  12902  ntrcls0  12925  neii1  12941  restbasg  12962  resttopon  12965  restuni2  12971  cnrest2r  13031  tx1cn  13063  txcnp  13065  txcn  13069  txswaphmeo  13115  psmettri  13124  xmeteq0  13153  xmettri  13166  metrtri  13171  ssblex  13225  xmeter  13230  isxms2  13246  cnbl0  13328  cnblcld  13329  reopnap  13332  tgioo  13340  addcncntoplem  13345  rescncf  13362  cncffvrn  13363  mulc1cncf  13370  cncfcncntop  13374  addccncf  13380  cdivcncfap  13381  negcncf  13382  cnopnap  13388  suplociccex  13397  limccl  13422  ellimc3apf  13423  cnplimcim  13430  limccnp2lem  13439  reldvg  13442  dvbsssg  13449  dvcjbr  13466  dvcj  13467  dvfre  13468  dvrecap  13471  dvef  13482  reeff1olem  13486  pilem3  13498  ptolemy  13539  rplogcl  13594  rpcxpef  13609  cxprec  13625  rpcxproot  13628  rplogb1  13660  logbgt0b  13678  logbgcd1irr  13679  binom4  13691  lgslem4  13698  lgsval  13699  lgsval2lem  13705  lgsval4a  13717  lgsdir2lem3  13725  lgsdir2  13728  lgsne0  13733  lgsprme0  13737  lgsmulsqcoprm  13741  bj-nnan  13771  bj-indind  13967  bj-omtrans  13991  bj-inf2vnlem1  14005  sscoll2  14023  pwtrufal  14030  sssneq  14035  pw1nct  14036  nninfsellemsuc  14045  nninfomnilem  14051  exmidsbthrlem  14054  qdencn  14059  trilpo  14075  trirec0  14076  apdiff  14080  iswomninnlem  14081  iswomni0  14083  redcwlpo  14087  redc0  14089  reap0  14090  dceqnconst  14091  dcapnconst  14092  neapmkv  14099