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  4182  undifexmid  4193  pwntru  4199  exmidundif  4206  exmidundifim  4207  opelopabsb  4260  sess1  4337  ordelord  4381  onin  4386  suctr  4421  abnexg  4446  ordtriexmidlem  4518  ordtri2or2exmid  4570  ontri2orexmidim  4571  tfi  4581  peano1  4593  peano2  4594  nnpredcl  4622  0nelxp  4654  0nelelxp  4655  brab2a  4679  mosubopt  4691  posng  4698  opabssxp  4700  ideqg  4778  relssres  4945  trin2  5020  dminss  5043  iota4an  5197  iota2  5206  iotam  5208  fun11uni  5286  imadiflem  5295  funimaexg  5300  fneq12  5309  fvelrnb  5563  dffo4  5664  ffnfv  5674  ffvresb  5679  fmptco  5682  fcoconst  5687  fcof1  5783  isotr  5816  isopolem  5822  f1oiso  5826  acexmidlemcase  5869  ovprc1  5910  fnoprabg  5975  op1steq  6179  dmmpog  6209  1stconst  6221  f1o2ndf1  6228  brtpos2  6251  tpostpos  6264  tposf12  6269  smores  6292  tfrlemi1  6332  tfr1onlembfn  6344  tfri1dALT  6351  tfrcllembfn  6357  freceq1  6392  freceq2  6393  frectfr  6400  omv2  6465  omsuc  6472  nnsucelsuc  6491  nntri3  6497  nnaordi  6508  nnmordi  6516  nnm00  6530  ecexr  6539  ertr  6549  swoer  6562  erth  6578  ecelqsdm  6604  iinerm  6606  ecinxp  6609  erovlem  6626  pmresg  6675  resixp  6732  elixpsn  6734  mapsnf1o  6736  dom3  6775  mapdom1g  6846  ssenen  6850  phpelm  6865  finexdc  6901  exmidpweq  6908  nnwetri  6914  fiintim  6927  ssfii  6972  fiss  6975  dcfi  6979  supubti  6997  supisoex  7007  ordiso2  7033  inl11  7063  omp1eomlem  7092  nnnninf  7123  nninfisol  7130  ctssexmid  7147  ismkvnex  7152  omniwomnimkv  7164  nninfwlpor  7171  nninfwlpoim  7175  en2eleq  7193  en2other2  7194  exmidfodomrlemr  7200  exmidfodomrlemrALT  7201  exmidaclem  7206  djuen  7209  djudoml  7217  netap  7252  2omotaplemst  7256  exmidapne  7258  cc1  7263  dmaddpqlem  7375  distrnqg  7385  ltanqi  7400  ltmnqi  7401  ltaddnq  7405  ltrnqg  7418  ltnnnq  7421  enq0sym  7430  addnq0mo  7445  mulnq0mo  7446  addnnnq0  7447  distrnq0  7457  prarloclemn  7497  prarloc  7501  ltdfpr  7504  genplt2i  7508  addnqprl  7527  addnqpru  7528  nqprl  7549  appdivnq  7561  1idprl  7588  1idpru  7589  ltexpri  7611  recexpr  7636  cauappcvgprlemdisj  7649  archrecpr  7662  addsrmo  7741  mulsrmo  7742  addsrpr  7743  mulsrpr  7744  0idsr  7765  1idsr  7766  archsr  7780  prsradd  7784  prsrlt  7785  caucvgsr  7800  map2psrprg  7803  elrealeu  7827  muladd11r  8112  negeu  8147  pncan  8162  pncan3  8164  negsub  8204  addid0  8329  posdif  8411  ltnegcon1  8419  subge0  8431  suble0  8432  lesub0  8435  reapval  8532  reapneg  8553  ap0gt0  8596  aprcl  8602  lt0ap0  8604  recextlem1  8607  recapb  8627  div0ap  8658  recrecap  8665  rec11ap  8666  recgt0  8806  mulgt1  8819  lerec2  8845  recp1lt1  8855  recreclt  8856  ledivp1  8859  negiso  8911  nnsub  8957  avglt1  9156  nnrecl  9173  nnnn0addcl  9205  elnn0nn  9217  nn0ge2m1nn  9235  zaddcl  9292  eluzadd  9555  infregelbex  9597  divfnzn  9620  qaddcl  9634  qreccl  9641  cnref1o  9649  ge0p1rp  9684  divlt1lt  9723  divle1le  9724  addlelt  9767  xrre3  9821  xltnegi  9834  xaddval  9844  xaddcom  9860  xnegdi  9867  xposdif  9881  ixxssixx  9901  iccshftr  9993  iccshftl  9995  iccdil  9997  icccntr  9999  zltaddlt1le  10006  elfz2  10014  peano2fzr  10036  fzdcel  10039  fzsplit2  10049  fzaddel  10058  fzrev2  10084  fzrev2i  10085  fzrev3  10086  elfz1b  10089  fseq1p1m1  10093  uzsubfz0  10128  fzosubel3  10195  eluzgtdifelfzo  10196  fzofzp1b  10227  elfzomelpfzo  10230  exfzdc  10239  fvinim0ffz  10240  exbtwnzlemshrink  10248  qbtwnz  10251  qbtwnxr  10257  ico0  10261  elicore  10266  apbtwnz  10273  flqge  10281  flqlt  10282  flqltnz  10286  flqbi2  10290  flqaddz  10296  flqmulnn0  10298  intfracq  10319  flqdiv  10320  q0mod  10354  q1mod  10355  mulp1mod1  10364  q2txmodxeq0  10383  modfzo0difsn  10394  frec2uzuzd  10401  frec2uzltd  10402  frec2uzrand  10404  uzennn  10435  seq3split  10478  seq3caopr  10482  exp3vallem  10520  exp3val  10521  expnnval  10522  exp1  10525  expcl2lemap  10531  rpexpcl  10538  expnegzap  10553  mulexp  10558  mulexpzap  10559  leexp2r  10573  leexp1a  10574  sq11  10592  subsq  10626  binom2  10631  binom3  10637  zesq  10638  bernneq  10640  sq11ap  10687  mulsubdivbinom2ap  10690  apexp1  10697  facwordi  10719  facubnd  10724  facavg  10725  bcval  10728  bcval5  10742  hashennn  10759  fihashf1rn  10767  fseq1hash  10780  hashdifsn  10798  hashdifpr  10799  hashxp  10805  fiubz  10808  fiubnn  10809  fnfz0hash  10811  ffzo0hash  10813  shftfvalg  10826  ovshftex  10827  shftdm  10830  shftfib  10831  shftval  10833  shftf  10838  crre  10865  cjexp  10901  cjreim2  10912  uzin2  10995  rexuz3  10998  resqrexlemgt0  11028  resqrex  11034  sqrtgt0  11042  sqrtsq  11052  sqrtmsq  11053  absrpclap  11069  absext  11071  absmul  11077  absid  11079  absexp  11087  nn0abscl  11093  abslt  11096  absle  11097  recvalap  11105  abstri  11112  caubnd2  11125  qdenre  11210  maxabsle  11212  maxabslemval  11216  maxcl  11218  rexanre  11228  min1inf  11239  minabs  11243  minclpr  11244  mul0inf  11248  mingeb  11249  xrmaxiflemcl  11252  xrnegiso  11269  climconst2  11298  climmpt  11307  climres  11310  climcaucn  11358  sumeq1  11362  summodclem2a  11388  isumz  11396  fisumss  11399  fsumzcl2  11412  sumsnf  11416  isumclim3  11430  fsum2dlemstep  11441  fisumcom2  11445  fsumconst  11461  cvgcmpub  11483  binom  11491  binom1p  11492  binom1dif  11494  bcxmas  11496  divcnv  11504  geo2lim  11523  geoisum  11524  geoisumr  11525  geoisum1  11526  mertenslemi1  11542  mertensabs  11544  prod1dc  11593  fprodconst  11627  fprodcom2fi  11633  efcllem  11666  efcj  11680  efadd  11682  efexp  11689  efgt1p2  11702  tanvalap  11715  tanval2ap  11720  tanval3ap  11721  sinadd  11743  cosadd  11744  dvdsdc  11804  iddvdsexp  11821  dvdsadd  11842  dvds1  11858  odd2np1  11877  oddm1even  11879  m1exp1  11905  divalglemnn  11922  fldivndvdslt  11939  flodddiv4lt  11940  zsupcllemex  11946  infssuzcldc  11951  dvdsbnd  11956  gcdnncl  11967  zeqzmulgcd  11970  gcdneg  11982  modgcd  11991  bezoutlemex  12001  bezoutlemeu  12007  dfgcd3  12010  gcdzeq  12022  dvdssq  12031  algrf  12044  eucalgval2  12052  eucalgcvga  12057  lcmval  12062  gcddvdslcm  12072  lcmneg  12073  coprmgcdb  12087  qredeu  12096  divgcdcoprm0  12100  divgcdcoprmex  12101  cncongr1  12102  cncongr2  12103  cncongrcoprm  12105  prmind2  12119  dvdsnprmd  12124  exprmfct  12137  isprm6  12146  pw2dvdslemn  12164  oddpwdclemdc  12172  sqrt2irraplemnn  12178  divnumden  12195  divdenle  12196  nn0sqrtelqelz  12205  phivalfi  12211  crth  12223  eulerth  12232  prmdivdiv  12236  reumodprminv  12252  nnnn0modprm0  12254  nnoddn2prmb  12261  pcval  12295  pcidlem  12321  pcid  12322  pcneg  12323  pc2dvds  12328  pcz  12330  pcprod  12343  prmpwdvds  12352  xpct  12396  znnen  12398  ennnfonelemg  12403  ennnfone  12425  ctinfom  12428  ctinf  12430  ssomct  12445  isstruct2im  12471  isstruct2r  12472  setsvalg  12491  setsslnid  12513  ressvalsets  12523  ressex  12524  2strbasg  12577  2stropg  12578  2strbas1g  12580  ressmulrg  12602  restval  12693  restid2  12696  prdsex  12717  fnpr2o  12757  xpsfval  12766  xpsval  12770  intopsn  12785  mgmidmo  12790  lidrididd  12800  ismnddef  12818  mndinvmod  12845  ismhm  12852  insubm  12871  dfgrp2  12901  grpsubval  12918  grpinvinv  12936  grpsubrcan  12950  grpsubadd  12957  grpaddsubass  12959  grpsubsub4  12962  grppnpcan2  12963  grpnpncan  12964  grpnpncan0  12965  grpnnncan2  12966  dfgrp3m  12968  dfgrp3me  12969  mhmmnd  12979  mulgfvalg  12984  mulgval  12985  mulgfng  12986  mulg1  12989  mulgnnp1  12990  mulgnndir  13010  mulgass  13018  mulgmodid  13020  issubg2m  13047  grpissubg  13052  isnsg  13060  isnsg3  13065  0nsg  13072  eqgfval  13079  eqger  13081  eqgen  13084  eqgcpbl  13085  abladdsub  13116  ablpncan3  13118  ablsubsub23  13126  mgpress  13139  srgmulgass  13170  srgrmhm  13175  isring  13181  rngo2times  13209  ringlz  13220  opprring  13247  mulgass3  13252  dvdsrd  13261  dvdsrneg  13270  unitnegcl  13297  dvrvald  13301  dvrid  13304  dvr1  13305  dvrass  13306  dvrdir  13310  ringinvdv  13312  ringelnzr  13326  issubrg2  13360  aprap  13374  lmodvs1  13404  dvdsrzring  13463  eltg2b  13524  difopn  13578  ntrcls0  13601  neii1  13617  restbasg  13638  resttopon  13641  restuni2  13647  cnrest2r  13707  tx1cn  13739  txcnp  13741  txcn  13745  txswaphmeo  13791  psmettri  13800  xmeteq0  13829  xmettri  13842  metrtri  13847  ssblex  13901  xmeter  13906  isxms2  13922  cnbl0  14004  cnblcld  14005  reopnap  14008  tgioo  14016  addcncntoplem  14021  rescncf  14038  cncfcdm  14039  mulc1cncf  14046  cncfcncntop  14050  addccncf  14056  cdivcncfap  14057  negcncf  14058  cnopnap  14064  suplociccex  14073  limccl  14098  ellimc3apf  14099  cnplimcim  14106  limccnp2lem  14115  reldvg  14118  dvbsssg  14125  dvcjbr  14142  dvcj  14143  dvfre  14144  dvrecap  14147  dvef  14158  reeff1olem  14162  pilem3  14174  ptolemy  14215  rplogcl  14270  rpcxpef  14285  cxprec  14301  rpcxproot  14304  rplogb1  14336  logbgt0b  14354  logbgcd1irr  14355  binom4  14367  lgslem4  14374  lgsval  14375  lgsval2lem  14381  lgsval4a  14393  lgsdir2lem3  14401  lgsdir2  14404  lgsne0  14409  lgsprme0  14413  lgsmulsqcoprm  14417  bj-nnan  14458  bj-indind  14654  bj-omtrans  14678  bj-inf2vnlem1  14692  sscoll2  14710  pwtrufal  14717  sssneq  14721  pw1nct  14722  nninfsellemsuc  14731  nninfomnilem  14737  exmidsbthrlem  14740  qdencn  14745  trilpo  14761  trirec0  14762  apdiff  14766  iswomninnlem  14767  iswomni0  14769  redcwlpo  14773  redc0  14775  reap0  14776  dceqnconst  14777  dcapnconst  14778  neapmkv  14785  neap0mkv  14786