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  3799  unissel  3837  ssmin  3862  abssexg  4180  undifexmid  4191  pwntru  4197  exmidundif  4204  exmidundifim  4205  opelopabsb  4258  sess1  4335  ordelord  4379  onin  4384  suctr  4419  abnexg  4444  ordtriexmidlem  4516  ordtri2or2exmid  4568  ontri2orexmidim  4569  tfi  4579  peano1  4591  peano2  4592  nnpredcl  4620  0nelxp  4652  0nelelxp  4653  brab2a  4677  mosubopt  4689  posng  4696  opabssxp  4698  ideqg  4775  relssres  4942  trin2  5017  dminss  5040  iota4an  5194  iota2  5203  iotam  5205  fun11uni  5283  imadiflem  5292  funimaexg  5297  fneq12  5306  fvelrnb  5560  dffo4  5661  ffnfv  5671  ffvresb  5676  fmptco  5679  fcoconst  5684  fcof1  5779  isotr  5812  isopolem  5818  f1oiso  5822  acexmidlemcase  5865  ovprc1  5906  fnoprabg  5971  op1steq  6175  dmmpog  6205  1stconst  6217  f1o2ndf1  6224  brtpos2  6247  tpostpos  6260  tposf12  6265  smores  6288  tfrlemi1  6328  tfr1onlembfn  6340  tfri1dALT  6347  tfrcllembfn  6353  freceq1  6388  freceq2  6389  frectfr  6396  omv2  6461  omsuc  6468  nnsucelsuc  6487  nntri3  6493  nnaordi  6504  nnmordi  6512  nnm00  6526  ecexr  6535  ertr  6545  swoer  6558  erth  6574  ecelqsdm  6600  iinerm  6602  ecinxp  6605  erovlem  6622  pmresg  6671  resixp  6728  elixpsn  6730  mapsnf1o  6732  dom3  6771  mapdom1g  6842  ssenen  6846  phpelm  6861  finexdc  6897  exmidpweq  6904  nnwetri  6910  fiintim  6923  ssfii  6968  fiss  6971  dcfi  6975  supubti  6993  supisoex  7003  ordiso2  7029  inl11  7059  omp1eomlem  7088  nnnninf  7119  nninfisol  7126  ctssexmid  7143  ismkvnex  7148  omniwomnimkv  7160  nninfwlpor  7167  nninfwlpoim  7171  en2eleq  7189  en2other2  7190  exmidfodomrlemr  7196  exmidfodomrlemrALT  7197  exmidaclem  7202  djuen  7205  djudoml  7213  netap  7248  2omotaplemst  7252  exmidapne  7254  cc1  7259  dmaddpqlem  7371  distrnqg  7381  ltanqi  7396  ltmnqi  7397  ltaddnq  7401  ltrnqg  7414  ltnnnq  7417  enq0sym  7426  addnq0mo  7441  mulnq0mo  7442  addnnnq0  7443  distrnq0  7453  prarloclemn  7493  prarloc  7497  ltdfpr  7500  genplt2i  7504  addnqprl  7523  addnqpru  7524  nqprl  7545  appdivnq  7557  1idprl  7584  1idpru  7585  ltexpri  7607  recexpr  7632  cauappcvgprlemdisj  7645  archrecpr  7658  addsrmo  7737  mulsrmo  7738  addsrpr  7739  mulsrpr  7740  0idsr  7761  1idsr  7762  archsr  7776  prsradd  7780  prsrlt  7781  caucvgsr  7796  map2psrprg  7799  elrealeu  7823  muladd11r  8107  negeu  8142  pncan  8157  pncan3  8159  negsub  8199  addid0  8324  posdif  8406  ltnegcon1  8414  subge0  8426  suble0  8427  lesub0  8430  reapval  8527  reapneg  8548  ap0gt0  8591  aprcl  8597  lt0ap0  8599  recextlem1  8602  recapb  8622  div0ap  8653  recrecap  8660  rec11ap  8661  recgt0  8801  mulgt1  8814  lerec2  8840  recp1lt1  8850  recreclt  8851  ledivp1  8854  negiso  8906  nnsub  8952  avglt1  9151  nnrecl  9168  nnnn0addcl  9200  elnn0nn  9212  nn0ge2m1nn  9230  zaddcl  9287  eluzadd  9550  infregelbex  9592  divfnzn  9615  qaddcl  9629  qreccl  9636  cnref1o  9644  ge0p1rp  9679  divlt1lt  9718  divle1le  9719  addlelt  9762  xrre3  9816  xltnegi  9829  xaddval  9839  xaddcom  9855  xnegdi  9862  xposdif  9876  ixxssixx  9896  iccshftr  9988  iccshftl  9990  iccdil  9992  icccntr  9994  zltaddlt1le  10001  elfz2  10009  peano2fzr  10030  fzdcel  10033  fzsplit2  10043  fzaddel  10052  fzrev2  10078  fzrev2i  10079  fzrev3  10080  elfz1b  10083  fseq1p1m1  10087  uzsubfz0  10122  fzosubel3  10189  eluzgtdifelfzo  10190  fzofzp1b  10221  elfzomelpfzo  10224  exfzdc  10233  fvinim0ffz  10234  exbtwnzlemshrink  10242  qbtwnz  10245  qbtwnxr  10251  ico0  10255  elicore  10260  apbtwnz  10267  flqge  10275  flqlt  10276  flqltnz  10280  flqbi2  10284  flqaddz  10290  flqmulnn0  10292  intfracq  10313  flqdiv  10314  q0mod  10348  q1mod  10349  mulp1mod1  10358  q2txmodxeq0  10377  modfzo0difsn  10388  frec2uzuzd  10395  frec2uzltd  10396  frec2uzrand  10398  uzennn  10429  seq3split  10472  seq3caopr  10476  exp3vallem  10514  exp3val  10515  expnnval  10516  exp1  10519  expcl2lemap  10525  rpexpcl  10532  expnegzap  10547  mulexp  10552  mulexpzap  10553  leexp2r  10567  leexp1a  10568  sq11  10585  subsq  10619  binom2  10624  binom3  10630  zesq  10631  bernneq  10633  sq11ap  10680  apexp1  10689  facwordi  10711  facubnd  10716  facavg  10717  bcval  10720  bcval5  10734  hashennn  10751  fihashf1rn  10759  fseq1hash  10772  hashdifsn  10790  hashdifpr  10791  hashxp  10797  fiubz  10800  fiubnn  10801  fnfz0hash  10803  ffzo0hash  10805  shftfvalg  10818  ovshftex  10819  shftdm  10822  shftfib  10823  shftval  10825  shftf  10830  crre  10857  cjexp  10893  cjreim2  10904  uzin2  10987  rexuz3  10990  resqrexlemgt0  11020  resqrex  11026  sqrtgt0  11034  sqrtsq  11044  sqrtmsq  11045  absrpclap  11061  absext  11063  absmul  11069  absid  11071  absexp  11079  nn0abscl  11085  abslt  11088  absle  11089  recvalap  11097  abstri  11104  caubnd2  11117  qdenre  11202  maxabsle  11204  maxabslemval  11208  maxcl  11210  rexanre  11220  min1inf  11231  minabs  11235  minclpr  11236  mul0inf  11240  mingeb  11241  xrmaxiflemcl  11244  xrnegiso  11261  climconst2  11290  climmpt  11299  climres  11302  climcaucn  11350  sumeq1  11354  summodclem2a  11380  isumz  11388  fisumss  11391  fsumzcl2  11404  sumsnf  11408  isumclim3  11422  fsum2dlemstep  11433  fisumcom2  11437  fsumconst  11453  cvgcmpub  11475  binom  11483  binom1p  11484  binom1dif  11486  bcxmas  11488  divcnv  11496  geo2lim  11515  geoisum  11516  geoisumr  11517  geoisum1  11518  mertenslemi1  11534  mertensabs  11536  prod1dc  11585  fprodconst  11619  fprodcom2fi  11625  efcllem  11658  efcj  11672  efadd  11674  efexp  11681  efgt1p2  11694  tanvalap  11707  tanval2ap  11712  tanval3ap  11713  sinadd  11735  cosadd  11736  dvdsdc  11796  iddvdsexp  11813  dvdsadd  11834  dvds1  11849  odd2np1  11868  oddm1even  11870  m1exp1  11896  divalglemnn  11913  fldivndvdslt  11930  flodddiv4lt  11931  zsupcllemex  11937  infssuzcldc  11942  dvdsbnd  11947  gcdnncl  11958  zeqzmulgcd  11961  gcdneg  11973  modgcd  11982  bezoutlemex  11992  bezoutlemeu  11998  dfgcd3  12001  gcdzeq  12013  dvdssq  12022  algrf  12035  eucalgval2  12043  eucalgcvga  12048  lcmval  12053  gcddvdslcm  12063  lcmneg  12064  coprmgcdb  12078  qredeu  12087  divgcdcoprm0  12091  divgcdcoprmex  12092  cncongr1  12093  cncongr2  12094  cncongrcoprm  12096  prmind2  12110  dvdsnprmd  12115  exprmfct  12128  isprm6  12137  pw2dvdslemn  12155  oddpwdclemdc  12163  sqrt2irraplemnn  12169  divnumden  12186  divdenle  12187  nn0sqrtelqelz  12196  phivalfi  12202  crth  12214  eulerth  12223  prmdivdiv  12227  reumodprminv  12243  nnnn0modprm0  12245  nnoddn2prmb  12252  pcval  12286  pcidlem  12312  pcid  12313  pcneg  12314  pc2dvds  12319  pcz  12321  pcprod  12334  prmpwdvds  12343  xpct  12387  znnen  12389  ennnfonelemg  12394  ennnfone  12416  ctinfom  12419  ctinf  12421  ssomct  12436  isstruct2im  12462  isstruct2r  12463  setsvalg  12482  setsslnid  12504  ressvalsets  12514  ressex  12515  2strbasg  12568  2stropg  12569  2strbas1g  12571  ressmulrg  12593  restval  12680  restid2  12683  intopsn  12716  mgmidmo  12721  lidrididd  12731  ismnddef  12749  mndinvmod  12774  ismhm  12781  insubm  12800  dfgrp2  12830  grpsubval  12847  grpinvinv  12865  grpsubrcan  12879  grpsubadd  12886  grpaddsubass  12888  grpsubsub4  12891  grppnpcan2  12892  grpnpncan  12893  grpnpncan0  12894  grpnnncan2  12895  dfgrp3m  12897  dfgrp3me  12898  mhmmnd  12908  mulgfvalg  12913  mulgval  12914  mulgfng  12915  mulg1  12918  mulgnnp1  12919  mulgnndir  12939  mulgass  12947  mulgmodid  12949  issubg2m  12975  grpissubg  12980  abladdsub  13018  ablpncan3  13020  ablsubsub23  13028  mgpress  13041  srgmulgass  13072  srgrmhm  13077  isring  13083  rngo2times  13111  ringlz  13122  opprring  13148  mulgass3  13153  dvdsrd  13162  dvdsrneg  13171  unitnegcl  13198  dvrvald  13202  dvrid  13205  dvr1  13206  dvrass  13207  dvrdir  13211  ringinvdv  13213  ringelnzr  13227  aprap  13243  eltg2b  13336  difopn  13390  ntrcls0  13413  neii1  13429  restbasg  13450  resttopon  13453  restuni2  13459  cnrest2r  13519  tx1cn  13551  txcnp  13553  txcn  13557  txswaphmeo  13603  psmettri  13612  xmeteq0  13641  xmettri  13654  metrtri  13659  ssblex  13713  xmeter  13718  isxms2  13734  cnbl0  13816  cnblcld  13817  reopnap  13820  tgioo  13828  addcncntoplem  13833  rescncf  13850  cncfcdm  13851  mulc1cncf  13858  cncfcncntop  13862  addccncf  13868  cdivcncfap  13869  negcncf  13870  cnopnap  13876  suplociccex  13885  limccl  13910  ellimc3apf  13911  cnplimcim  13918  limccnp2lem  13927  reldvg  13930  dvbsssg  13937  dvcjbr  13954  dvcj  13955  dvfre  13956  dvrecap  13959  dvef  13970  reeff1olem  13974  pilem3  13986  ptolemy  14027  rplogcl  14082  rpcxpef  14097  cxprec  14113  rpcxproot  14116  rplogb1  14148  logbgt0b  14166  logbgcd1irr  14167  binom4  14179  lgslem4  14186  lgsval  14187  lgsval2lem  14193  lgsval4a  14205  lgsdir2lem3  14213  lgsdir2  14216  lgsne0  14221  lgsprme0  14225  lgsmulsqcoprm  14229  bj-nnan  14259  bj-indind  14455  bj-omtrans  14479  bj-inf2vnlem1  14493  sscoll2  14511  pwtrufal  14518  sssneq  14522  pw1nct  14523  nninfsellemsuc  14532  nninfomnilem  14538  exmidsbthrlem  14541  qdencn  14546  trilpo  14562  trirec0  14563  apdiff  14567  iswomninnlem  14568  iswomni0  14570  redcwlpo  14574  redc0  14576  reap0  14577  dceqnconst  14578  dcapnconst  14579  neapmkv  14586  neap0mkv  14587