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  696  ioran  753  pm3.14  754  pm4.44  780  ordi  817  pm4.39  823  animorl  824  animorlr  826  pm5.16  829  pm5.54dc  919  intnanr  931  intnanrd  933  dcan  935  dedlema  971  dedlemb  972  pm4.42r  973  prlem2  976  simp1l  1023  simp2l  1025  simp3l  1027  3anandis  1358  xordc1  1404  anxordi  1411  falantru  1414  19.26  1492  exsimpl  1628  sbequ2  1780  sbcof2  1821  sbequilem  1849  sbequ8  1858  euan  2098  mooran1  2114  eupickbi  2124  2exeu  2134  dimatis  2159  rexim  2588  r19.26  2620  r19.40  2648  rspcime  2871  rr19.28v  2900  elrab3t  2915  eueq3dc  2934  mosubt  2937  reu6  2949  sbc2iegf  3056  sbcralt  3062  sbcrext  3063  rmob  3078  csbiebt  3120  ssab2  3263  difdif  3284  uneqin  3410  indifdir  3415  undif3ss  3420  rexm  3546  eqifdc  3592  ifandc  3595  ifnebibdc  3600  difsn  3755  opprc1  3826  unissel  3864  ssmin  3889  abssexg  4211  undifexmid  4222  pwntru  4228  exmidundif  4235  exmidundifim  4236  opelopabsb  4290  sess1  4368  ordelord  4412  onin  4417  suctr  4452  abnexg  4477  ifexg  4516  ordtriexmidlem  4551  ordtri2or2exmid  4603  ontri2orexmidim  4604  tfi  4614  peano1  4626  peano2  4627  nnpredcl  4655  0nelxp  4687  0nelelxp  4688  brab2a  4712  mosubopt  4724  posng  4731  opabssxp  4733  ideqg  4813  relssres  4980  trin2  5057  dminss  5080  iota4an  5235  iota2  5244  iotam  5246  fun11uni  5324  imadiflem  5333  funimaexg  5338  fneq12  5347  fvelrnb  5604  dffo4  5706  ffnfv  5716  ffvresb  5721  fmptco  5724  fcoconst  5729  fcof1  5826  isotr  5859  isopolem  5865  f1oiso  5869  acexmidlemcase  5913  ovprc1  5954  fnoprabg  6019  elovmporab  6118  elovmporab1w  6119  uchoice  6190  op1steq  6232  dmmpog  6262  1stconst  6274  f1o2ndf1  6281  brtpos2  6304  tpostpos  6317  tposf12  6322  smores  6345  tfrlemi1  6385  tfr1onlembfn  6397  tfri1dALT  6404  tfrcllembfn  6410  freceq1  6445  freceq2  6446  frectfr  6453  omv2  6518  omsuc  6525  nnsucelsuc  6544  nntri3  6550  nnaordi  6561  nnmordi  6569  nnm00  6583  ecexr  6592  ertr  6602  swoer  6615  erth  6633  ecelqsdm  6659  iinerm  6661  ecinxp  6664  erovlem  6681  pmresg  6730  resixp  6787  elixpsn  6789  mapsnf1o  6791  dom3  6830  mapdom1g  6903  ssenen  6907  phpelm  6922  finexdc  6958  exmidpweq  6965  nnwetri  6972  fiintim  6985  infidc  6993  ssfii  7033  fiss  7036  dcfi  7040  supubti  7058  supisoex  7068  ordiso2  7094  inl11  7124  omp1eomlem  7153  nnnninf  7185  nninfisol  7192  ctssexmid  7209  ismkvnex  7214  omniwomnimkv  7226  nninfwlpor  7233  nninfwlpoim  7237  en2eleq  7255  en2other2  7256  exmidfodomrlemr  7262  exmidfodomrlemrALT  7263  exmidaclem  7268  djuen  7271  djudoml  7279  netap  7314  2omotaplemst  7318  exmidapne  7320  cc1  7325  dmaddpqlem  7437  distrnqg  7447  ltanqi  7462  ltmnqi  7463  ltaddnq  7467  ltrnqg  7480  ltnnnq  7483  enq0sym  7492  addnq0mo  7507  mulnq0mo  7508  addnnnq0  7509  distrnq0  7519  prarloclemn  7559  prarloc  7563  ltdfpr  7566  genplt2i  7570  addnqprl  7589  addnqpru  7590  nqprl  7611  appdivnq  7623  1idprl  7650  1idpru  7651  ltexpri  7673  recexpr  7698  cauappcvgprlemdisj  7711  archrecpr  7724  addsrmo  7803  mulsrmo  7804  addsrpr  7805  mulsrpr  7806  0idsr  7827  1idsr  7828  archsr  7842  prsradd  7846  prsrlt  7847  caucvgsr  7862  map2psrprg  7865  elrealeu  7889  muladd11r  8175  negeu  8210  pncan  8225  pncan3  8227  negsub  8267  addid0  8392  posdif  8474  ltnegcon1  8482  subge0  8494  suble0  8495  lesub0  8498  reapval  8595  reapneg  8616  ap0gt0  8659  aprcl  8665  lt0ap0  8667  recextlem1  8670  recapb  8690  div0ap  8721  recrecap  8728  rec11ap  8729  recgt0  8869  mulgt1  8882  lerec2  8908  recp1lt1  8918  recreclt  8919  ledivp1  8922  negiso  8974  nnsub  9021  avglt1  9221  nnrecl  9238  nnnn0addcl  9270  elnn0nn  9282  nn0ge2m1nn  9300  zaddcl  9357  eluzadd  9621  infregelbex  9663  divfnzn  9686  qaddcl  9700  qreccl  9707  cnref1o  9716  ge0p1rp  9751  divlt1lt  9790  divle1le  9791  addlelt  9834  xrre3  9888  xltnegi  9901  xaddval  9911  xaddcom  9927  xnegdi  9934  xposdif  9948  ixxssixx  9968  iccshftr  10060  iccshftl  10062  iccdil  10064  icccntr  10066  zltaddlt1le  10073  elfz2  10081  peano2fzr  10103  fzdcel  10106  fzsplit2  10116  fzaddel  10125  fzrev2  10151  fzrev2i  10152  fzrev3  10153  elfz1b  10156  fseq1p1m1  10160  uzsubfz0  10195  fzosubel3  10263  eluzgtdifelfzo  10264  fzofzp1b  10295  elfzomelpfzo  10298  exfzdc  10307  fvinim0ffz  10308  exbtwnzlemshrink  10317  qbtwnz  10320  qbtwnxr  10326  ico0  10330  elicore  10335  xqltnle  10336  apbtwnz  10343  flqge  10351  flqlt  10352  flqltnz  10356  flqbi2  10360  flqaddz  10366  flqmulnn0  10368  intfracq  10391  flqdiv  10392  q0mod  10426  q1mod  10427  mulp1mod1  10436  q2txmodxeq0  10455  modfzo0difsn  10466  frec2uzuzd  10473  frec2uzltd  10474  frec2uzrand  10476  uzennn  10507  seqfveq2g  10548  seq3split  10559  seqsplitg  10560  seq3caopr  10566  seqcaoprg  10567  seqf1oglem2  10591  seqf1og  10592  exp3vallem  10611  exp3val  10612  expnnval  10613  exp1  10616  expcl2lemap  10622  rpexpcl  10629  expnegzap  10644  mulexp  10649  mulexpzap  10650  leexp2r  10664  leexp1a  10665  sq11  10683  subsq  10717  binom2  10722  binom3  10728  zesq  10729  bernneq  10731  sq11ap  10778  zzlesq  10779  mulsubdivbinom2ap  10782  apexp1  10789  facwordi  10811  facubnd  10816  facavg  10817  bcval  10820  bcval5  10834  hashennn  10851  fihashf1rn  10859  fseq1hash  10872  hashdifsn  10890  hashdifpr  10891  hashxp  10897  fiubz  10900  fiubnn  10901  fnfz0hash  10903  ffzo0hash  10905  wrdval  10917  wrdsymb0  10946  shftfvalg  10962  ovshftex  10963  shftdm  10966  shftfib  10967  shftval  10969  shftf  10974  crre  11001  cjexp  11037  cjreim2  11048  uzin2  11131  rexuz3  11134  resqrexlemgt0  11164  resqrex  11170  sqrtgt0  11178  sqrtsq  11188  sqrtmsq  11189  absrpclap  11205  absext  11207  absmul  11213  absid  11215  absexp  11223  nn0abscl  11229  abslt  11232  absle  11233  recvalap  11241  abstri  11248  caubnd2  11261  qdenre  11346  maxabsle  11348  maxabslemval  11352  maxcl  11354  rexanre  11364  min1inf  11375  minabs  11379  minclpr  11380  mul0inf  11384  mingeb  11385  xrmaxiflemcl  11388  xrnegiso  11405  climconst2  11434  climmpt  11443  climres  11446  climcaucn  11494  sumeq1  11498  summodclem2a  11524  isumz  11532  fisumss  11535  fsumzcl2  11548  sumsnf  11552  isumclim3  11566  fsum2dlemstep  11577  fisumcom2  11581  fsumconst  11597  cvgcmpub  11619  binom  11627  binom1p  11628  binom1dif  11630  bcxmas  11632  divcnv  11640  geo2lim  11659  geoisum  11660  geoisumr  11661  geoisum1  11662  mertenslemi1  11678  mertensabs  11680  prod1dc  11729  fprodconst  11763  fprodcom2fi  11769  efcllem  11802  efcj  11816  efadd  11818  efexp  11825  efgt1p2  11838  tanvalap  11851  tanval2ap  11856  tanval3ap  11857  sinadd  11879  cosadd  11880  dvdsdc  11941  iddvdsexp  11958  dvdsadd  11979  dvds1  11995  odd2np1  12014  oddm1even  12016  m1exp1  12042  divalglemnn  12059  fldivndvdslt  12076  flodddiv4lt  12077  zsupcllemex  12083  infssuzcldc  12088  dvdsbnd  12093  gcdnncl  12104  zeqzmulgcd  12107  gcdneg  12119  modgcd  12128  bezoutlemex  12138  bezoutlemeu  12144  dfgcd3  12147  gcdzeq  12159  dvdssq  12168  algrf  12183  eucalgval2  12191  eucalgcvga  12196  lcmval  12201  gcddvdslcm  12211  lcmneg  12212  coprmgcdb  12226  qredeu  12235  divgcdcoprm0  12239  divgcdcoprmex  12240  cncongr1  12241  cncongr2  12242  cncongrcoprm  12244  prmind2  12258  dvdsnprmd  12263  exprmfct  12276  isprm6  12285  pw2dvdslemn  12303  oddpwdclemdc  12311  sqrt2irraplemnn  12317  divnumden  12334  divdenle  12335  nn0sqrtelqelz  12344  phivalfi  12350  crth  12362  eulerth  12371  prmdivdiv  12375  reumodprminv  12391  nnnn0modprm0  12393  nnoddn2prmb  12400  pcval  12434  pcidlem  12461  pcid  12462  pcneg  12463  pc2dvds  12468  pcz  12470  pcprod  12484  prmpwdvds  12493  4sqexercise1  12536  xpct  12553  znnen  12555  ennnfonelemg  12560  ennnfone  12582  ctinfom  12585  ctinf  12587  ssomct  12602  isstruct2im  12628  isstruct2r  12629  setsvalg  12648  setsslnid  12670  ressvalsets  12682  ressex  12683  2strbasg  12737  2stropg  12738  2strbas1g  12740  ressmulrg  12762  ressscag  12800  ressvscag  12801  ressipg  12802  restval  12856  restid2  12859  prdsex  12880  qusex  12908  fnpr2o  12922  xpsfval  12931  xpsval  12935  intopsn  12950  mgmidmo  12955  lidrididd  12965  ismnddef  12999  mndinvmod  13026  ismhm  13033  mhmex  13034  insubm  13057  dfgrp2  13099  grpsubval  13118  grpinvinv  13139  grpsubrcan  13153  grpsubadd  13160  grpaddsubass  13162  grpsubsub4  13165  grppnpcan2  13166  grpnpncan  13167  grpnpncan0  13168  grpnnncan2  13169  dfgrp3m  13171  dfgrp3me  13172  imasgrp2  13180  mhmmnd  13186  mulgfvalg  13191  mulgval  13192  mulgfng  13194  mulg1  13199  mulgnnp1  13200  mulgnndir  13221  mulgass  13229  mulgmodid  13231  issubg2m  13259  grpissubg  13264  isnsg  13272  isnsg3  13277  0nsg  13284  eqgfval  13292  eqger  13294  eqgen  13297  eqgcpbl  13298  quseccl  13303  isghm  13313  kerf1ghm  13344  conjghm  13346  conjsubg  13347  abladdsub  13385  ablpncan3  13387  ablsubsub23  13395  invghm  13399  subgabl  13402  mgpress  13427  rngdi  13436  rnglz  13441  imasrng  13452  srgmulgass  13485  srgrmhm  13490  isring  13496  ringo2times  13524  ringrng  13532  ringlz  13539  imasring  13560  opprrng  13573  opprrngbg  13574  opprring  13575  mulgass3  13581  dvdsrd  13590  dvdsrneg  13599  unitnegcl  13626  dvrvald  13630  dvrid  13633  dvr1  13634  dvrass  13635  dvrdir  13639  ringinvdv  13641  rhmex  13653  isrim0  13657  rhmval  13669  rhmdvdsr  13671  rhmopp  13672  elrhmunit  13673  rhmunitinv  13674  isnzr2  13680  ringelnzr  13683  issubrng2  13706  issubrg2  13737  aprap  13782  lmodvs1  13812  lmod0vs  13817  lmodvs0  13818  lmodvsmmulgdi  13819  lmodfopne  13822  lmodvneg1  13826  lss1  13858  islss3  13875  lsslss  13877  lss1d  13879  lspf  13885  lspsn  13912  lspsnneg  13916  sraval  13933  sraring  13945  qus1  14022  qusrhm  14024  cnfldui  14077  dvdsrzring  14091  mulgghm2  14096  mulgrhm  14097  znval  14124  znf1o  14139  psrplusgg  14162  eltg2b  14222  difopn  14276  ntrcls0  14299  neii1  14315  restbasg  14336  resttopon  14339  restuni2  14345  cnrest2r  14405  tx1cn  14437  txcnp  14439  txcn  14443  txswaphmeo  14489  psmettri  14498  xmeteq0  14527  xmettri  14540  metrtri  14545  ssblex  14599  xmeter  14604  isxms2  14620  cnbl0  14702  cnblcld  14703  reopnap  14706  tgioo  14714  addcncntoplem  14719  rescncf  14736  cncfcdm  14737  mulc1cncf  14744  cncfcncntop  14748  addccncf  14754  cdivcncfap  14758  negcncf  14759  cnopnap  14765  suplociccex  14779  hoverlt1  14803  hovergt0  14804  dich0  14806  limccl  14813  ellimc3apf  14814  cnplimcim  14821  limccnp2lem  14830  reldvg  14833  dvbsssg  14840  dvcjbr  14857  dvcj  14858  dvfre  14859  dvrecap  14862  dvef  14873  plyaddcl  14900  plymulcl  14901  plysubcl  14902  reeff1olem  14906  pilem3  14918  ptolemy  14959  rplogcl  15014  rpcxpef  15029  cxprec  15045  rpcxproot  15048  rplogb1  15080  logbgt0b  15098  logbgcd1irr  15099  binom4  15111  wilthlem1  15112  lgslem4  15119  lgsval  15120  lgsval2lem  15126  lgsval4a  15138  lgsdir2lem3  15146  lgsdir2  15149  lgsne0  15154  lgsprme0  15158  lgsmulsqcoprm  15162  gausslemma2dlem0a  15165  gausslemma2dlem1a  15174  bj-nnan  15228  bj-indind  15424  bj-omtrans  15448  bj-inf2vnlem1  15462  sscoll2  15480  pwtrufal  15488  sssneq  15492  pw1nct  15493  nninfsellemsuc  15502  nninfomnilem  15508  exmidsbthrlem  15512  qdencn  15517  trilpo  15533  trirec0  15534  apdiff  15538  iswomninnlem  15539  iswomni0  15541  redcwlpo  15545  redc0  15547  reap0  15548  cndcap  15549  dceqnconst  15550  dcapnconst  15551  neapmkv  15558  neap0mkv  15559