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  469  adantrr  471  adantllr  473  adantlrr  475  adantrlr  477  adantrrr  479  simplll  523  simplrl  525  simprll  527  simprrl  529  anabs1  562  jcab  593  pm4.38  595  pm5.21  685  ioran  742  pm3.14  743  pm4.44  769  ordi  806  pm4.39  812  pm5.16  814  pm5.54dc  904  intnanr  916  intnanrd  918  dcan  919  dedlema  954  dedlemb  955  pm4.42r  956  prlem2  959  simp1l  1006  simp2l  1008  simp3l  1010  3anandis  1329  xordc1  1375  anxordi  1382  falantru  1385  19.26  1461  exsimpl  1597  sbequ2  1749  sbcof2  1790  sbequilem  1818  sbequ8  1827  euan  2062  mooran1  2078  eupickbi  2088  2exeu  2098  dimatis  2123  rexim  2551  r19.26  2583  r19.40  2611  rspcime  2823  rr19.28v  2852  elrab3t  2867  eueq3dc  2886  mosubt  2889  reu6  2901  sbc2iegf  3007  sbcralt  3013  sbcrext  3014  rmob  3029  csbiebt  3070  ssab2  3212  difdif  3232  uneqin  3358  indifdir  3363  undif3ss  3368  rexm  3493  eqifdc  3539  ifandc  3541  difsn  3693  opprc1  3763  unissel  3801  ssmin  3826  abssexg  4143  undifexmid  4154  pwntru  4160  exmidundif  4167  exmidundifim  4168  opelopabsb  4220  sess1  4297  ordelord  4341  onin  4346  suctr  4381  abnexg  4406  ordtriexmidlem  4478  ordtri2or2exmid  4530  ontri2orexmidim  4531  tfi  4541  peano1  4553  peano2  4554  nnpredcl  4582  0nelxp  4614  0nelelxp  4615  brab2a  4639  mosubopt  4651  posng  4658  opabssxp  4660  ideqg  4737  relssres  4904  trin2  4977  dminss  5000  iota4an  5154  iota2  5161  fun11uni  5240  imadiflem  5249  funimaexg  5254  fneq12  5263  fvelrnb  5516  dffo4  5615  ffnfv  5625  ffvresb  5630  fmptco  5633  fcoconst  5638  fcof1  5733  isotr  5766  isopolem  5772  f1oiso  5776  acexmidlemcase  5819  ovprc1  5857  fnoprabg  5922  op1steq  6127  dmmpog  6157  1stconst  6168  f1o2ndf1  6175  brtpos2  6198  tpostpos  6211  tposf12  6216  smores  6239  tfrlemi1  6279  tfr1onlembfn  6291  tfri1dALT  6298  tfrcllembfn  6304  freceq1  6339  freceq2  6340  frectfr  6347  omv2  6412  omsuc  6419  nnsucelsuc  6438  nntri3  6444  nnaordi  6455  nnmordi  6463  nnm00  6476  ecexr  6485  ertr  6495  swoer  6508  erth  6524  ecelqsdm  6550  iinerm  6552  ecinxp  6555  erovlem  6572  pmresg  6621  resixp  6678  elixpsn  6680  mapsnf1o  6682  dom3  6721  mapdom1g  6792  ssenen  6796  phpelm  6811  finexdc  6847  exmidpweq  6854  nnwetri  6860  fiintim  6873  ssfii  6918  fiss  6921  dcfi  6925  supubti  6943  supisoex  6953  ordiso2  6979  inl11  7009  omp1eomlem  7038  nnnninf  7069  nninfisol  7076  ctssexmid  7093  ismkvnex  7098  omniwomnimkv  7110  en2eleq  7130  en2other2  7131  exmidfodomrlemr  7137  exmidfodomrlemrALT  7138  exmidaclem  7143  djuen  7146  djudoml  7154  cc1  7185  dmaddpqlem  7297  distrnqg  7307  ltanqi  7322  ltmnqi  7323  ltaddnq  7327  ltrnqg  7340  ltnnnq  7343  enq0sym  7352  addnq0mo  7367  mulnq0mo  7368  addnnnq0  7369  distrnq0  7379  prarloclemn  7419  prarloc  7423  ltdfpr  7426  genplt2i  7430  addnqprl  7449  addnqpru  7450  nqprl  7471  appdivnq  7483  1idprl  7510  1idpru  7511  ltexpri  7533  recexpr  7558  cauappcvgprlemdisj  7571  archrecpr  7584  addsrmo  7663  mulsrmo  7664  addsrpr  7665  mulsrpr  7666  0idsr  7687  1idsr  7688  archsr  7702  prsradd  7706  prsrlt  7707  caucvgsr  7722  map2psrprg  7725  elrealeu  7749  muladd11r  8031  negeu  8066  pncan  8081  pncan3  8083  negsub  8123  addid0  8248  posdif  8330  ltnegcon1  8338  subge0  8350  suble0  8351  lesub0  8354  reapval  8451  reapneg  8472  ap0gt0  8515  aprcl  8521  lt0ap0  8523  recextlem1  8525  div0ap  8575  recrecap  8582  rec11ap  8583  recgt0  8721  mulgt1  8734  lerec2  8760  recp1lt1  8770  recreclt  8771  ledivp1  8774  negiso  8826  nnsub  8872  avglt1  9071  nnrecl  9088  nnnn0addcl  9120  elnn0nn  9132  nn0ge2m1nn  9150  zaddcl  9207  eluzadd  9467  infregelbex  9509  divfnzn  9530  qaddcl  9544  qreccl  9551  cnref1o  9559  ge0p1rp  9592  divlt1lt  9631  divle1le  9632  addlelt  9675  xrre3  9726  xltnegi  9739  xaddval  9749  xaddcom  9765  xnegdi  9772  xposdif  9786  ixxssixx  9806  iccshftr  9898  iccshftl  9900  iccdil  9902  icccntr  9904  zltaddlt1le  9911  elfz2  9919  peano2fzr  9939  fzdcel  9942  fzsplit2  9952  fzaddel  9961  fzrev2  9987  fzrev2i  9988  fzrev3  9989  elfz1b  9992  fseq1p1m1  9996  uzsubfz0  10028  fzosubel3  10095  eluzgtdifelfzo  10096  fzofzp1b  10127  elfzomelpfzo  10130  exfzdc  10139  fvinim0ffz  10140  exbtwnzlemshrink  10148  qbtwnz  10151  qbtwnxr  10157  ico0  10161  elicore  10166  apbtwnz  10173  flqge  10181  flqlt  10182  flqltnz  10186  flqbi2  10190  flqaddz  10196  flqmulnn0  10198  intfracq  10219  flqdiv  10220  q0mod  10254  q1mod  10255  mulp1mod1  10264  q2txmodxeq0  10283  modfzo0difsn  10294  frec2uzuzd  10301  frec2uzltd  10302  frec2uzrand  10304  uzennn  10335  seq3split  10378  seq3caopr  10382  exp3vallem  10420  exp3val  10421  expnnval  10422  exp1  10425  expcl2lemap  10431  rpexpcl  10438  expnegzap  10453  mulexp  10458  mulexpzap  10459  leexp2r  10473  leexp1a  10474  sq11  10491  subsq  10525  binom2  10529  binom3  10535  zesq  10536  bernneq  10538  sq11ap  10585  apexp1  10592  facwordi  10614  facubnd  10619  facavg  10620  bcval  10623  bcval5  10637  hashennn  10654  fihashf1rn  10663  fseq1hash  10675  hashdifsn  10693  hashdifpr  10694  hashxp  10700  fnfz0hash  10703  ffzo0hash  10705  shftfvalg  10718  ovshftex  10719  shftdm  10722  shftfib  10723  shftval  10725  shftf  10730  crre  10757  cjexp  10793  cjreim2  10804  uzin2  10887  rexuz3  10890  resqrexlemgt0  10920  resqrex  10926  sqrtgt0  10934  sqrtsq  10944  sqrtmsq  10945  absrpclap  10961  absext  10963  absmul  10969  absid  10971  absexp  10979  nn0abscl  10985  abslt  10988  absle  10989  recvalap  10997  abstri  11004  caubnd2  11017  qdenre  11102  maxabsle  11104  maxabslemval  11108  maxcl  11110  rexanre  11120  min1inf  11131  minabs  11135  minclpr  11136  mul0inf  11140  xrmaxiflemcl  11142  xrnegiso  11159  climconst2  11188  climmpt  11197  climres  11200  climcaucn  11248  sumeq1  11252  summodclem2a  11278  isumz  11286  fisumss  11289  fsumzcl2  11302  sumsnf  11306  isumclim3  11320  fsum2dlemstep  11331  fisumcom2  11335  fsumconst  11351  cvgcmpub  11373  binom  11381  binom1p  11382  binom1dif  11384  bcxmas  11386  divcnv  11394  geo2lim  11413  geoisum  11414  geoisumr  11415  geoisum1  11416  mertenslemi1  11432  mertensabs  11434  prod1dc  11483  fprodconst  11517  fprodcom2fi  11523  efcllem  11556  efcj  11570  efadd  11572  efexp  11579  efgt1p2  11592  tanvalap  11605  tanval2ap  11610  tanval3ap  11611  sinadd  11633  cosadd  11634  dvdsdc  11694  iddvdsexp  11710  dvdsadd  11729  dvds1  11744  odd2np1  11763  oddm1even  11765  m1exp1  11791  divalglemnn  11808  fldivndvdslt  11825  flodddiv4lt  11826  zsupcllemex  11832  infssuzcldc  11837  dvdsbnd  11839  gcdnncl  11850  zeqzmulgcd  11853  gcdneg  11865  modgcd  11874  bezoutlemex  11884  bezoutlemeu  11890  dfgcd3  11893  gcdzeq  11905  dvdssq  11914  algrf  11921  eucalgval2  11929  eucalgcvga  11934  lcmval  11939  gcddvdslcm  11949  lcmneg  11950  coprmgcdb  11964  qredeu  11973  divgcdcoprm0  11977  divgcdcoprmex  11978  cncongr1  11979  cncongr2  11980  cncongrcoprm  11982  prmind2  11996  dvdsnprmd  12001  exprmfct  12014  isprm6  12021  pw2dvdslemn  12039  oddpwdclemdc  12047  sqrt2irraplemnn  12053  divnumden  12070  divdenle  12071  nn0sqrtelqelz  12080  phivalfi  12086  crth  12098  eulerth  12107  prmdivdiv  12111  xpct  12125  znnen  12127  ennnfonelemg  12132  ennnfone  12154  ctinfom  12157  ctinf  12159  ssomct  12174  isstruct2im  12200  isstruct2r  12201  setsvalg  12220  setsslnid  12241  ressid2  12249  ressval2  12250  2strbasg  12291  2stropg  12292  2strbas1g  12294  restval  12357  restid2  12360  eltg2b  12454  difopn  12508  ntrcls0  12531  neii1  12547  restbasg  12568  resttopon  12571  restuni2  12577  cnrest2r  12637  tx1cn  12669  txcnp  12671  txcn  12675  txswaphmeo  12721  psmettri  12730  xmeteq0  12759  xmettri  12772  metrtri  12777  ssblex  12831  xmeter  12836  isxms2  12852  cnbl0  12934  cnblcld  12935  reopnap  12938  tgioo  12946  addcncntoplem  12951  rescncf  12968  cncffvrn  12969  mulc1cncf  12976  cncfcncntop  12980  addccncf  12986  cdivcncfap  12987  negcncf  12988  cnopnap  12994  suplociccex  13003  limccl  13028  ellimc3apf  13029  cnplimcim  13036  limccnp2lem  13045  reldvg  13048  dvbsssg  13055  dvcjbr  13072  dvcj  13073  dvfre  13074  dvrecap  13077  dvef  13088  reeff1olem  13092  pilem3  13104  ptolemy  13145  rplogcl  13200  rpcxpef  13215  cxprec  13231  rpcxproot  13234  rplogb1  13265  logbgt0b  13283  logbgcd1irr  13284  binom4  13296  bj-nnan  13312  bj-indind  13507  bj-omtrans  13531  bj-inf2vnlem1  13545  sscoll2  13563  pwtrufal  13569  sssneq  13574  pw1nct  13575  nninfsellemsuc  13584  nninfomnilem  13590  exmidsbthrlem  13593  qdencn  13598  trilpo  13614  trirec0  13615  apdiff  13619  iswomninnlem  13620  iswomni0  13622  redcwlpo  13626  redc0  13628  reap0  13629  dceqnconst  13630  dcapnconst  13631  neapmkv  13638