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  605  pm4.38  607  pm5.21  700  ioran  757  pm3.14  758  pm4.44  784  ordi  821  pm4.39  827  animorl  828  animorlr  830  pm5.16  833  pm5.54dc  923  intnanr  935  intnanrd  937  dcan  939  dedlema  975  dedlemb  976  pm4.42r  977  prlem2  980  ifpdc  985  dfifp2dc  987  simp1l  1045  simp2l  1047  simp3l  1049  3anandis  1381  xordc1  1435  anxordi  1442  falantru  1445  19.26  1527  exsimpl  1663  sbequ2  1815  sbcof2  1856  sbequilem  1884  sbequ8  1893  euan  2134  mooran1  2150  eupickbi  2160  2exeu  2170  dimatis  2195  rexim  2624  r19.26  2657  r19.40  2685  rspcime  2915  rr19.28v  2944  elrab3t  2959  eueq3dc  2978  mosubt  2981  reu6  2993  sbc2iegf  3100  sbcralt  3106  sbcrext  3107  rmob  3123  csbiebt  3165  ssab2  3309  difdif  3330  uneqin  3456  indifdir  3461  undif3ss  3466  rexm  3592  eqifdc  3640  ifandc  3644  ifnebibdc  3649  difsn  3808  opprc1  3882  unissel  3920  ssmin  3945  abssexg  4270  undifexmid  4281  pwntru  4287  exmidundif  4294  exmidundifim  4295  opelopabsb  4352  elopabran  4376  sess1  4432  ordelord  4476  onin  4481  suctr  4516  abnexg  4541  ifexg  4580  ordtriexmidlem  4615  ordtri2or2exmid  4667  ontri2orexmidim  4668  tfi  4678  peano1  4690  peano2  4691  nnpredcl  4719  0nelxp  4751  0nelelxp  4752  brab2a  4777  mosubopt  4789  posng  4796  opabssxp  4798  ideqg  4879  relssres  5049  trin2  5126  dminss  5149  iota4an  5305  iota2  5314  iotam  5316  fununfun  5370  fun11uni  5397  imadiflem  5406  funimaexg  5411  fneq12  5420  fvelrnb  5689  dffo4  5791  ffnfv  5801  ffvresb  5806  fmptco  5809  fcoconst  5814  funopsn  5825  fcof1  5919  isotr  5952  isopolem  5958  f1oiso  5962  acexmidlemcase  6008  ovprc1  6050  fnoprabg  6117  elovmporab  6217  elovmporab1w  6218  uchoice  6295  op1steq  6337  dmmpog  6369  1stconst  6381  f1o2ndf1  6388  brtpos2  6412  tpostpos  6425  tposf12  6430  smores  6453  tfrlemi1  6493  tfr1onlembfn  6505  tfri1dALT  6512  tfrcllembfn  6518  freceq1  6553  freceq2  6554  frectfr  6561  omv2  6628  omsuc  6635  nnsucelsuc  6654  nntri3  6660  nnaordi  6671  nnmordi  6679  nnm00  6693  ecexr  6702  ertr  6712  swoer  6725  erth  6743  ecelqsdm  6769  iinerm  6771  ecinxp  6774  erovlem  6791  pmresg  6840  resixp  6897  elixpsn  6899  mapsnf1o  6901  dom3  6944  modom  6989  mapdom1g  7028  ssenen  7032  phpelm  7048  finexdc  7085  exmidpweq  7094  nnwetri  7101  fiintim  7116  infidc  7124  ssfii  7164  fiss  7167  dcfi  7171  supubti  7189  supisoex  7199  ordiso2  7225  inl11  7255  omp1eomlem  7284  nnnninf  7316  nninfisol  7323  ctssexmid  7340  ismkvnex  7345  omniwomnimkv  7357  nninfwlpor  7364  nninfwlpoim  7369  nninfinfwlpo  7370  en2eleq  7396  en2other2  7397  exmidfodomrlemr  7403  exmidfodomrlemrALT  7404  acnrcl  7406  exmidaclem  7413  djuen  7416  djudoml  7424  netap  7463  2omotaplemst  7467  exmidapne  7469  cc1  7474  acnccim  7481  dmaddpqlem  7587  distrnqg  7597  ltanqi  7612  ltmnqi  7613  ltaddnq  7617  ltrnqg  7630  ltnnnq  7633  enq0sym  7642  addnq0mo  7657  mulnq0mo  7658  addnnnq0  7659  distrnq0  7669  prarloclemn  7709  prarloc  7713  ltdfpr  7716  genplt2i  7720  addnqprl  7739  addnqpru  7740  nqprl  7761  appdivnq  7773  1idprl  7800  1idpru  7801  ltexpri  7823  recexpr  7848  cauappcvgprlemdisj  7861  archrecpr  7874  addsrmo  7953  mulsrmo  7954  addsrpr  7955  mulsrpr  7956  0idsr  7977  1idsr  7978  archsr  7992  prsradd  7996  prsrlt  7997  caucvgsr  8012  map2psrprg  8015  elrealeu  8039  muladd11r  8325  negeu  8360  pncan  8375  pncan3  8377  negsub  8417  addid0  8542  posdif  8625  ltnegcon1  8633  subge0  8645  suble0  8646  lesub0  8649  reapval  8746  reapneg  8767  ap0gt0  8810  aprcl  8816  lt0ap0  8818  recextlem1  8821  recapb  8841  div0ap  8872  recrecap  8879  rec11ap  8880  recgt0  9020  mulgt1  9033  lerec2  9059  recp1lt1  9069  recreclt  9070  ledivp1  9073  negiso  9125  nnsub  9172  avglt1  9373  nnrecl  9390  nnnn0addcl  9422  elnn0nn  9434  nn0ge2m1nn  9452  zaddcl  9509  eluzmn  9752  eluzadd  9775  infregelbex  9822  divfnzn  9845  qaddcl  9859  qreccl  9866  cnref1o  9875  ge0p1rp  9910  divlt1lt  9949  divle1le  9950  addlelt  9993  xrre3  10047  xltnegi  10060  xaddval  10070  xaddcom  10086  xnegdi  10093  xposdif  10107  ixxssixx  10127  iccshftr  10219  iccshftl  10221  iccdil  10223  icccntr  10225  zltaddlt1le  10232  elfz2  10240  peano2fzr  10262  fzdcel  10265  fzsplit2  10275  fzaddel  10284  fzrev2  10310  fzrev2i  10311  fzrev3  10312  elfz1b  10315  fseq1p1m1  10319  uzsubfz0  10354  fzosubel3  10431  eluzgtdifelfzo  10432  fzofzp1b  10463  elfzomelpfzo  10466  exfzdc  10476  fvinim0ffz  10477  zsupcllemex  10480  infssuzcldc  10485  exbtwnzlemshrink  10498  qbtwnz  10501  qbtwnxr  10507  ico0  10511  elicore  10516  xqltnle  10517  apbtwnz  10524  flqge  10532  flqlt  10533  flqltnz  10537  flqbi2  10541  flqaddz  10547  flqmulnn0  10549  intfracq  10572  flqdiv  10573  q0mod  10607  q1mod  10608  mulp1mod1  10617  q2txmodxeq0  10636  modfzo0difsn  10647  frec2uzuzd  10654  frec2uzltd  10655  frec2uzrand  10657  uzennn  10688  seqfveq2g  10729  seq3split  10740  seqsplitg  10741  seq3caopr  10747  seqcaoprg  10748  seqf1oglem2  10772  seqf1og  10773  exp3vallem  10792  exp3val  10793  expnnval  10794  exp1  10797  expcl2lemap  10803  rpexpcl  10810  expnegzap  10825  mulexp  10830  mulexpzap  10831  leexp2r  10845  leexp1a  10846  sq11  10864  subsq  10898  binom2  10903  binom3  10909  zesq  10910  bernneq  10912  sq11ap  10959  zzlesq  10960  mulsubdivbinom2ap  10963  apexp1  10970  facwordi  10992  facubnd  10997  facavg  10998  bcval  11001  bcval5  11015  hashennn  11032  fihashf1rn  11040  fseq1hash  11054  hashdifsn  11073  hashdifpr  11074  hashxp  11080  fiubz  11083  fiubnn  11084  fnfz0hash  11086  ffzo0hash  11088  hash2en  11097  wrdval  11106  ffz0iswrdnn0  11130  wrdsymb0  11136  ccatsymb  11169  ccatval21sw  11172  lswccatn0lsw  11178  ccatalpha  11180  ccatrcl1  11181  s111  11198  ccat1st1st  11208  lswccats1fst  11211  swrdlen2  11233  swrdfv2  11234  swrdsbslen  11237  swrds1  11239  ccatswrd  11241  pfxval  11245  pfxclg  11249  pfxmpt  11251  pfxid  11257  pfxfv0  11263  pfxtrcfv0  11265  pfxfvlsw  11266  pfxeq  11267  ccatpfx  11272  swrdpfx  11278  lenrevpfxcctswrd  11283  wrdeqs1cat  11291  cats1un  11292  swrdccatin1  11296  pfxccatin12lem2a  11298  pfxccatin12lem1  11299  pfxccatin12lem3  11303  pfxccatin12  11304  swrdccat  11306  pfxccat3a  11309  swrdccat3blem  11310  swrdccat3b  11311  reuccatpfxs1lem  11317  reuccatpfxs1  11318  s2cl  11356  s2fv0g  11358  shftfvalg  11369  ovshftex  11370  shftdm  11373  shftfib  11374  shftval  11376  shftf  11381  crre  11408  cjexp  11444  cjreim2  11455  uzin2  11538  rexuz3  11541  resqrexlemgt0  11571  resqrex  11577  sqrtgt0  11585  sqrtsq  11595  sqrtmsq  11596  absrpclap  11612  absext  11614  absmul  11620  absid  11622  absexp  11630  nn0abscl  11636  abslt  11639  absle  11640  recvalap  11648  abstri  11655  caubnd2  11668  qdenre  11753  maxabsle  11755  maxabslemval  11759  maxcl  11761  rexanre  11771  min1inf  11783  minabs  11787  minclpr  11788  mul0inf  11792  mingeb  11793  xrmaxiflemcl  11796  xrnegiso  11813  climconst2  11842  climmpt  11851  climres  11854  climcaucn  11902  sumeq1  11906  summodclem2a  11932  isumz  11940  fisumss  11943  fsumzcl2  11956  sumsnf  11960  isumclim3  11974  fsum2dlemstep  11985  fisumcom2  11989  fsumconst  12005  cvgcmpub  12027  binom  12035  binom1p  12036  binom1dif  12038  bcxmas  12040  divcnv  12048  geo2lim  12067  geoisum  12068  geoisumr  12069  geoisum1  12070  mertenslemi1  12086  mertensabs  12088  prod1dc  12137  fprodconst  12171  fprodcom2fi  12177  efcllem  12210  efcj  12224  efadd  12226  efexp  12233  efgt1p2  12246  tanvalap  12259  tanval2ap  12264  tanval3ap  12265  sinadd  12287  cosadd  12288  dvdsdc  12349  iddvdsexp  12366  dvdsadd  12387  dvds1  12404  odd2np1  12424  oddm1even  12426  m1exp1  12452  divalglemnn  12469  fldivndvdslt  12488  flodddiv4lt  12489  bitsp1  12502  bitsmod  12507  bitsfi  12508  bitscmp  12509  bitsinv1lem  12512  dvdsbnd  12517  gcdnncl  12528  zeqzmulgcd  12531  gcdneg  12543  modgcd  12552  bezoutlemex  12562  bezoutlemeu  12568  dfgcd3  12571  gcdzeq  12583  dvdssq  12592  algrf  12607  eucalgval2  12615  eucalgcvga  12620  lcmval  12625  gcddvdslcm  12635  lcmneg  12636  coprmgcdb  12650  qredeu  12659  divgcdcoprm0  12663  divgcdcoprmex  12664  cncongr1  12665  cncongr2  12666  cncongrcoprm  12668  prmind2  12682  dvdsnprmd  12687  exprmfct  12700  isprm6  12709  pw2dvdslemn  12727  oddpwdclemdc  12735  sqrt2irraplemnn  12741  divnumden  12758  divdenle  12759  nn0sqrtelqelz  12768  phivalfi  12774  crth  12786  eulerth  12795  prmdivdiv  12799  reumodprminv  12816  nnnn0modprm0  12818  nnoddn2prmb  12825  pcval  12859  pcidlem  12886  pcid  12887  pcneg  12888  pc2dvds  12893  pcz  12895  pcprod  12909  prmpwdvds  12918  4sqexercise1  12961  2expltfac  13002  xpct  13007  znnen  13009  ennnfonelemg  13014  ennnfone  13036  ctinfom  13039  ctinf  13041  ssomct  13056  isstruct2im  13082  isstruct2r  13083  setsvalg  13102  setsslnid  13124  ressvalsets  13137  ressex  13138  2strbasg  13193  2stropg  13194  2strbas1g  13196  ressmulrg  13218  ressscag  13256  ressvscag  13257  ressipg  13258  restval  13318  restid2  13321  prdsex  13342  pwsval  13364  qusex  13398  fnpr2o  13412  xpsfval  13421  xpsval  13425  intopsn  13440  mgmidmo  13445  lidrididd  13455  ismnddef  13491  mndinvmod  13518  imasmnd2  13525  ismhm  13534  mhmex  13535  insubm  13558  dfgrp2  13600  grpsubval  13619  grpinvinv  13640  grpsubrcan  13654  grpsubadd  13661  grpaddsubass  13663  grpsubsub4  13666  grppnpcan2  13667  grpnpncan  13668  grpnpncan0  13669  grpnnncan2  13670  dfgrp3m  13672  dfgrp3me  13673  imasgrp2  13687  mhmmnd  13693  mulgfvalg  13698  mulgval  13699  mulgfng  13701  mulg1  13706  mulgnnp1  13707  mulgnndir  13728  mulgass  13736  mulgmodid  13738  issubg2m  13766  grpissubg  13771  isnsg  13779  isnsg3  13784  0nsg  13791  eqgfval  13799  eqger  13801  eqgen  13804  eqgcpbl  13805  quseccl  13810  isghm  13820  kerf1ghm  13851  conjghm  13853  conjsubg  13854  abladdsub  13892  ablpncan3  13894  ablsubsub23  13902  invghm  13906  subgabl  13909  mgpress  13934  rngdi  13943  rnglz  13948  imasrng  13959  srgmulgass  13992  srgrmhm  13997  isring  14003  ringo2times  14031  ringrng  14039  ringlz  14046  imasring  14067  opprrng  14080  opprrngbg  14081  opprring  14082  mulgass3  14088  dvdsrd  14098  dvdsrneg  14107  unitnegcl  14134  dvrvald  14138  dvrid  14141  dvr1  14142  dvrass  14143  dvrdir  14147  ringinvdv  14149  rhmex  14161  isrim0  14165  rhmval  14177  rhmdvdsr  14179  rhmopp  14180  elrhmunit  14181  rhmunitinv  14182  isnzr2  14188  ringelnzr  14191  issubrng2  14214  issubrg2  14245  aprap  14290  lmodvs1  14320  lmod0vs  14325  lmodvs0  14326  lmodvsmmulgdi  14327  lmodfopne  14330  lmodvneg1  14334  lss1  14366  islss3  14383  lsslss  14385  lss1d  14387  lspf  14393  lspsn  14420  lspsnneg  14424  sraval  14441  sraring  14453  qus1  14530  qusrhm  14532  cnfldui  14593  dvdsrzring  14607  mulgghm2  14612  mulgrhm  14613  znval  14640  znf1o  14655  psrbagfi  14677  psrplusgg  14682  mplgrpfi  14710  eltg2b  14768  difopn  14822  ntrcls0  14845  neii1  14861  restbasg  14882  resttopon  14885  restuni2  14891  cnrest2r  14951  tx1cn  14983  txcnp  14985  txcn  14989  txswaphmeo  15035  psmettri  15044  xmeteq0  15073  xmettri  15086  metrtri  15091  ssblex  15145  xmeter  15150  isxms2  15166  cnbl0  15248  cnblcld  15249  reopnap  15260  tgioo  15268  addcncntoplem  15275  expcn  15283  rescncf  15295  cncfcdm  15296  mulc1cncf  15303  cncfcncntop  15307  addccncf  15314  cdivcncfap  15318  negcncf  15319  cnopnap  15325  suplociccex  15339  hoverlt1  15363  hovergt0  15364  dich0  15366  limccl  15373  ellimc3apf  15374  cnplimcim  15381  limccnp2lem  15390  reldvg  15393  dvbsssg  15400  dvcjbr  15422  dvcj  15423  dvfre  15424  dvrecap  15427  dvef  15441  plyaddcl  15468  plymulcl  15469  plysubcl  15470  plyrecj  15477  reeff1olem  15485  pilem3  15497  ptolemy  15538  rplogcl  15593  rpcxpef  15608  cxprec  15624  rpcxproot  15628  rplogb1  15662  logbgt0b  15680  logbgcd1irr  15681  binom4  15693  wilthlem1  15694  sgmnncl  15702  dvdsppwf1o  15703  mersenne  15711  lgslem4  15722  lgsval  15723  lgsval2lem  15729  lgsval4a  15741  lgsdir2lem3  15749  lgsdir2  15752  lgsne0  15757  lgsprme0  15761  lgsmulsqcoprm  15765  gausslemma2dlem0a  15768  gausslemma2dlem1a  15777  2lgslem1b  15808  2lgslem2  15811  2lgsoddprm  15832  struct2slots2dom  15879  structvtxval  15880  structiedg0val  15881  struct2griedg  15887  edgstruct  15905  uhgr0vb  15925  incistruhgr  15931  umgrvad2edg  16050  uspgredg2vlem  16059  uspgredg2v  16060  usgredg2v  16063  ushgredgedg  16065  ushgredgedgloop  16067  usgr0vb  16072  uhgr0vusgr  16077  edg0usgr  16086  vtxdgfval  16094  wksfval  16119  wlkpropg  16121  uspgr2wlkeq2  16163  uspgr2wlkeqi  16164  upgr2wlkdc  16172  trlsex  16182  clwwlkccatlem  16195  clwwlkng  16200  clwwlkext2edg  16217  clwwlknccat  16218  umgr2cwwkdifex  16220  clwwlknonel  16227  clwwlknonccat  16228  clwwlknonex2lem2  16233  clwwlknun  16236  eupthsg  16240  bj-nnan  16268  bj-indind  16463  bj-omtrans  16487  bj-inf2vnlem1  16501  sscoll2  16519  2omap  16530  pw1map  16532  pwtrufal  16534  sssneq  16539  pw1nct  16540  nninfsellemsuc  16550  nninfomnilem  16556  nnnninfex  16560  exmidsbthrlem  16562  qdencn  16567  trilpo  16583  trirec0  16584  apdiff  16588  iswomninnlem  16589  iswomni0  16591  redcwlpo  16595  redc0  16597  reap0  16598  cndcap  16599  dceqnconst  16600  dcapnconst  16601  neapmkv  16608  neap0mkv  16609