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  697  ioran  754  pm3.14  755  pm4.44  781  ordi  818  pm4.39  824  animorl  825  animorlr  827  pm5.16  830  pm5.54dc  920  intnanr  932  intnanrd  934  dcan  936  dedlema  972  dedlemb  973  pm4.42r  974  prlem2  977  simp1l  1024  simp2l  1026  simp3l  1028  3anandis  1360  xordc1  1413  anxordi  1420  falantru  1423  19.26  1504  exsimpl  1640  sbequ2  1792  sbcof2  1833  sbequilem  1861  sbequ8  1870  euan  2110  mooran1  2126  eupickbi  2136  2exeu  2146  dimatis  2171  rexim  2600  r19.26  2632  r19.40  2660  rspcime  2884  rr19.28v  2913  elrab3t  2928  eueq3dc  2947  mosubt  2950  reu6  2962  sbc2iegf  3069  sbcralt  3075  sbcrext  3076  rmob  3091  csbiebt  3133  ssab2  3277  difdif  3298  uneqin  3424  indifdir  3429  undif3ss  3434  rexm  3560  eqifdc  3607  ifandc  3610  ifnebibdc  3615  difsn  3770  opprc1  3841  unissel  3879  ssmin  3904  abssexg  4226  undifexmid  4237  pwntru  4243  exmidundif  4250  exmidundifim  4251  opelopabsb  4306  sess1  4384  ordelord  4428  onin  4433  suctr  4468  abnexg  4493  ifexg  4532  ordtriexmidlem  4567  ordtri2or2exmid  4619  ontri2orexmidim  4620  tfi  4630  peano1  4642  peano2  4643  nnpredcl  4671  0nelxp  4703  0nelelxp  4704  brab2a  4728  mosubopt  4740  posng  4747  opabssxp  4749  ideqg  4829  relssres  4997  trin2  5074  dminss  5097  iota4an  5252  iota2  5261  iotam  5263  fununfun  5317  fun11uni  5344  imadiflem  5353  funimaexg  5358  fneq12  5367  fvelrnb  5626  dffo4  5728  ffnfv  5738  ffvresb  5743  fmptco  5746  fcoconst  5751  funopsn  5762  fcof1  5852  isotr  5885  isopolem  5891  f1oiso  5895  acexmidlemcase  5939  ovprc1  5981  fnoprabg  6046  elovmporab  6146  elovmporab1w  6147  uchoice  6223  op1steq  6265  dmmpog  6295  1stconst  6307  f1o2ndf1  6314  brtpos2  6337  tpostpos  6350  tposf12  6355  smores  6378  tfrlemi1  6418  tfr1onlembfn  6430  tfri1dALT  6437  tfrcllembfn  6443  freceq1  6478  freceq2  6479  frectfr  6486  omv2  6551  omsuc  6558  nnsucelsuc  6577  nntri3  6583  nnaordi  6594  nnmordi  6602  nnm00  6616  ecexr  6625  ertr  6635  swoer  6648  erth  6666  ecelqsdm  6692  iinerm  6694  ecinxp  6697  erovlem  6714  pmresg  6763  resixp  6820  elixpsn  6822  mapsnf1o  6824  dom3  6867  mapdom1g  6944  ssenen  6948  phpelm  6963  finexdc  6999  exmidpweq  7006  nnwetri  7013  fiintim  7028  infidc  7036  ssfii  7076  fiss  7079  dcfi  7083  supubti  7101  supisoex  7111  ordiso2  7137  inl11  7167  omp1eomlem  7196  nnnninf  7228  nninfisol  7235  ctssexmid  7252  ismkvnex  7257  omniwomnimkv  7269  nninfwlpor  7276  nninfwlpoim  7281  nninfinfwlpo  7282  en2eleq  7303  en2other2  7304  exmidfodomrlemr  7310  exmidfodomrlemrALT  7311  acnrcl  7313  exmidaclem  7320  djuen  7323  djudoml  7331  netap  7366  2omotaplemst  7370  exmidapne  7372  cc1  7377  acnccim  7384  dmaddpqlem  7490  distrnqg  7500  ltanqi  7515  ltmnqi  7516  ltaddnq  7520  ltrnqg  7533  ltnnnq  7536  enq0sym  7545  addnq0mo  7560  mulnq0mo  7561  addnnnq0  7562  distrnq0  7572  prarloclemn  7612  prarloc  7616  ltdfpr  7619  genplt2i  7623  addnqprl  7642  addnqpru  7643  nqprl  7664  appdivnq  7676  1idprl  7703  1idpru  7704  ltexpri  7726  recexpr  7751  cauappcvgprlemdisj  7764  archrecpr  7777  addsrmo  7856  mulsrmo  7857  addsrpr  7858  mulsrpr  7859  0idsr  7880  1idsr  7881  archsr  7895  prsradd  7899  prsrlt  7900  caucvgsr  7915  map2psrprg  7918  elrealeu  7942  muladd11r  8228  negeu  8263  pncan  8278  pncan3  8280  negsub  8320  addid0  8445  posdif  8528  ltnegcon1  8536  subge0  8548  suble0  8549  lesub0  8552  reapval  8649  reapneg  8670  ap0gt0  8713  aprcl  8719  lt0ap0  8721  recextlem1  8724  recapb  8744  div0ap  8775  recrecap  8782  rec11ap  8783  recgt0  8923  mulgt1  8936  lerec2  8962  recp1lt1  8972  recreclt  8973  ledivp1  8976  negiso  9028  nnsub  9075  avglt1  9276  nnrecl  9293  nnnn0addcl  9325  elnn0nn  9337  nn0ge2m1nn  9355  zaddcl  9412  eluzadd  9677  infregelbex  9719  divfnzn  9742  qaddcl  9756  qreccl  9763  cnref1o  9772  ge0p1rp  9807  divlt1lt  9846  divle1le  9847  addlelt  9890  xrre3  9944  xltnegi  9957  xaddval  9967  xaddcom  9983  xnegdi  9990  xposdif  10004  ixxssixx  10024  iccshftr  10116  iccshftl  10118  iccdil  10120  icccntr  10122  zltaddlt1le  10129  elfz2  10137  peano2fzr  10159  fzdcel  10162  fzsplit2  10172  fzaddel  10181  fzrev2  10207  fzrev2i  10208  fzrev3  10209  elfz1b  10212  fseq1p1m1  10216  uzsubfz0  10251  fzosubel3  10325  eluzgtdifelfzo  10326  fzofzp1b  10357  elfzomelpfzo  10360  exfzdc  10369  fvinim0ffz  10370  zsupcllemex  10373  infssuzcldc  10378  exbtwnzlemshrink  10391  qbtwnz  10394  qbtwnxr  10400  ico0  10404  elicore  10409  xqltnle  10410  apbtwnz  10417  flqge  10425  flqlt  10426  flqltnz  10430  flqbi2  10434  flqaddz  10440  flqmulnn0  10442  intfracq  10465  flqdiv  10466  q0mod  10500  q1mod  10501  mulp1mod1  10510  q2txmodxeq0  10529  modfzo0difsn  10540  frec2uzuzd  10547  frec2uzltd  10548  frec2uzrand  10550  uzennn  10581  seqfveq2g  10622  seq3split  10633  seqsplitg  10634  seq3caopr  10640  seqcaoprg  10641  seqf1oglem2  10665  seqf1og  10666  exp3vallem  10685  exp3val  10686  expnnval  10687  exp1  10690  expcl2lemap  10696  rpexpcl  10703  expnegzap  10718  mulexp  10723  mulexpzap  10724  leexp2r  10738  leexp1a  10739  sq11  10757  subsq  10791  binom2  10796  binom3  10802  zesq  10803  bernneq  10805  sq11ap  10852  zzlesq  10853  mulsubdivbinom2ap  10856  apexp1  10863  facwordi  10885  facubnd  10890  facavg  10891  bcval  10894  bcval5  10908  hashennn  10925  fihashf1rn  10933  fseq1hash  10946  hashdifsn  10964  hashdifpr  10965  hashxp  10971  fiubz  10974  fiubnn  10975  fnfz0hash  10977  ffzo0hash  10979  hash2en  10988  wrdval  10997  wrdsymb0  11026  ccatsymb  11058  ccatval21sw  11061  lswccatn0lsw  11067  s111  11085  ccat1st1st  11093  lswccats1fst  11096  swrdlen2  11115  swrdfv2  11116  swrdsbslen  11119  swrds1  11121  ccatswrd  11123  shftfvalg  11129  ovshftex  11130  shftdm  11133  shftfib  11134  shftval  11136  shftf  11141  crre  11168  cjexp  11204  cjreim2  11215  uzin2  11298  rexuz3  11301  resqrexlemgt0  11331  resqrex  11337  sqrtgt0  11345  sqrtsq  11355  sqrtmsq  11356  absrpclap  11372  absext  11374  absmul  11380  absid  11382  absexp  11390  nn0abscl  11396  abslt  11399  absle  11400  recvalap  11408  abstri  11415  caubnd2  11428  qdenre  11513  maxabsle  11515  maxabslemval  11519  maxcl  11521  rexanre  11531  min1inf  11543  minabs  11547  minclpr  11548  mul0inf  11552  mingeb  11553  xrmaxiflemcl  11556  xrnegiso  11573  climconst2  11602  climmpt  11611  climres  11614  climcaucn  11662  sumeq1  11666  summodclem2a  11692  isumz  11700  fisumss  11703  fsumzcl2  11716  sumsnf  11720  isumclim3  11734  fsum2dlemstep  11745  fisumcom2  11749  fsumconst  11765  cvgcmpub  11787  binom  11795  binom1p  11796  binom1dif  11798  bcxmas  11800  divcnv  11808  geo2lim  11827  geoisum  11828  geoisumr  11829  geoisum1  11830  mertenslemi1  11846  mertensabs  11848  prod1dc  11897  fprodconst  11931  fprodcom2fi  11937  efcllem  11970  efcj  11984  efadd  11986  efexp  11993  efgt1p2  12006  tanvalap  12019  tanval2ap  12024  tanval3ap  12025  sinadd  12047  cosadd  12048  dvdsdc  12109  iddvdsexp  12126  dvdsadd  12147  dvds1  12164  odd2np1  12184  oddm1even  12186  m1exp1  12212  divalglemnn  12229  fldivndvdslt  12248  flodddiv4lt  12249  bitsp1  12262  bitsmod  12267  bitsfi  12268  bitscmp  12269  bitsinv1lem  12272  dvdsbnd  12277  gcdnncl  12288  zeqzmulgcd  12291  gcdneg  12303  modgcd  12312  bezoutlemex  12322  bezoutlemeu  12328  dfgcd3  12331  gcdzeq  12343  dvdssq  12352  algrf  12367  eucalgval2  12375  eucalgcvga  12380  lcmval  12385  gcddvdslcm  12395  lcmneg  12396  coprmgcdb  12410  qredeu  12419  divgcdcoprm0  12423  divgcdcoprmex  12424  cncongr1  12425  cncongr2  12426  cncongrcoprm  12428  prmind2  12442  dvdsnprmd  12447  exprmfct  12460  isprm6  12469  pw2dvdslemn  12487  oddpwdclemdc  12495  sqrt2irraplemnn  12501  divnumden  12518  divdenle  12519  nn0sqrtelqelz  12528  phivalfi  12534  crth  12546  eulerth  12555  prmdivdiv  12559  reumodprminv  12576  nnnn0modprm0  12578  nnoddn2prmb  12585  pcval  12619  pcidlem  12646  pcid  12647  pcneg  12648  pc2dvds  12653  pcz  12655  pcprod  12669  prmpwdvds  12678  4sqexercise1  12721  2expltfac  12762  xpct  12767  znnen  12769  ennnfonelemg  12774  ennnfone  12796  ctinfom  12799  ctinf  12801  ssomct  12816  isstruct2im  12842  isstruct2r  12843  setsvalg  12862  setsslnid  12884  ressvalsets  12896  ressex  12897  2strbasg  12952  2stropg  12953  2strbas1g  12955  ressmulrg  12977  ressscag  13015  ressvscag  13016  ressipg  13017  restval  13077  restid2  13080  prdsex  13101  pwsval  13123  qusex  13157  fnpr2o  13171  xpsfval  13180  xpsval  13184  intopsn  13199  mgmidmo  13204  lidrididd  13214  ismnddef  13250  mndinvmod  13277  imasmnd2  13284  ismhm  13293  mhmex  13294  insubm  13317  dfgrp2  13359  grpsubval  13378  grpinvinv  13399  grpsubrcan  13413  grpsubadd  13420  grpaddsubass  13422  grpsubsub4  13425  grppnpcan2  13426  grpnpncan  13427  grpnpncan0  13428  grpnnncan2  13429  dfgrp3m  13431  dfgrp3me  13432  imasgrp2  13446  mhmmnd  13452  mulgfvalg  13457  mulgval  13458  mulgfng  13460  mulg1  13465  mulgnnp1  13466  mulgnndir  13487  mulgass  13495  mulgmodid  13497  issubg2m  13525  grpissubg  13530  isnsg  13538  isnsg3  13543  0nsg  13550  eqgfval  13558  eqger  13560  eqgen  13563  eqgcpbl  13564  quseccl  13569  isghm  13579  kerf1ghm  13610  conjghm  13612  conjsubg  13613  abladdsub  13651  ablpncan3  13653  ablsubsub23  13661  invghm  13665  subgabl  13668  mgpress  13693  rngdi  13702  rnglz  13707  imasrng  13718  srgmulgass  13751  srgrmhm  13756  isring  13762  ringo2times  13790  ringrng  13798  ringlz  13805  imasring  13826  opprrng  13839  opprrngbg  13840  opprring  13841  mulgass3  13847  dvdsrd  13856  dvdsrneg  13865  unitnegcl  13892  dvrvald  13896  dvrid  13899  dvr1  13900  dvrass  13901  dvrdir  13905  ringinvdv  13907  rhmex  13919  isrim0  13923  rhmval  13935  rhmdvdsr  13937  rhmopp  13938  elrhmunit  13939  rhmunitinv  13940  isnzr2  13946  ringelnzr  13949  issubrng2  13972  issubrg2  14003  aprap  14048  lmodvs1  14078  lmod0vs  14083  lmodvs0  14084  lmodvsmmulgdi  14085  lmodfopne  14088  lmodvneg1  14092  lss1  14124  islss3  14141  lsslss  14143  lss1d  14145  lspf  14151  lspsn  14178  lspsnneg  14182  sraval  14199  sraring  14211  qus1  14288  qusrhm  14290  cnfldui  14351  dvdsrzring  14365  mulgghm2  14370  mulgrhm  14371  znval  14398  znf1o  14413  psrbagfi  14435  psrplusgg  14440  mplgrpfi  14468  eltg2b  14526  difopn  14580  ntrcls0  14603  neii1  14619  restbasg  14640  resttopon  14643  restuni2  14649  cnrest2r  14709  tx1cn  14741  txcnp  14743  txcn  14747  txswaphmeo  14793  psmettri  14802  xmeteq0  14831  xmettri  14844  metrtri  14849  ssblex  14903  xmeter  14908  isxms2  14924  cnbl0  15006  cnblcld  15007  reopnap  15018  tgioo  15026  addcncntoplem  15033  expcn  15041  rescncf  15053  cncfcdm  15054  mulc1cncf  15061  cncfcncntop  15065  addccncf  15072  cdivcncfap  15076  negcncf  15077  cnopnap  15083  suplociccex  15097  hoverlt1  15121  hovergt0  15122  dich0  15124  limccl  15131  ellimc3apf  15132  cnplimcim  15139  limccnp2lem  15148  reldvg  15151  dvbsssg  15158  dvcjbr  15180  dvcj  15181  dvfre  15182  dvrecap  15185  dvef  15199  plyaddcl  15226  plymulcl  15227  plysubcl  15228  plyrecj  15235  reeff1olem  15243  pilem3  15255  ptolemy  15296  rplogcl  15351  rpcxpef  15366  cxprec  15382  rpcxproot  15386  rplogb1  15420  logbgt0b  15438  logbgcd1irr  15439  binom4  15451  wilthlem1  15452  sgmnncl  15460  dvdsppwf1o  15461  mersenne  15469  lgslem4  15480  lgsval  15481  lgsval2lem  15487  lgsval4a  15499  lgsdir2lem3  15507  lgsdir2  15510  lgsne0  15515  lgsprme0  15519  lgsmulsqcoprm  15523  gausslemma2dlem0a  15526  gausslemma2dlem1a  15535  2lgslem1b  15566  2lgslem2  15569  2lgsoddprm  15590  struct2slots2dom  15635  structvtxval  15636  structiedg0val  15637  struct2griedg  15643  edgstruct  15656  bj-nnan  15672  bj-indind  15868  bj-omtrans  15892  bj-inf2vnlem1  15906  sscoll2  15924  2omap  15932  pwtrufal  15934  sssneq  15939  pw1nct  15940  nninfsellemsuc  15949  nninfomnilem  15955  nnnninfex  15959  exmidsbthrlem  15961  qdencn  15966  trilpo  15982  trirec0  15983  apdiff  15987  iswomninnlem  15988  iswomni0  15990  redcwlpo  15994  redc0  15996  reap0  15997  cndcap  15998  dceqnconst  15999  dcapnconst  16000  neapmkv  16007  neap0mkv  16008