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	⊢ ((𝜑 ∧ 𝜓) → 𝜑)

Proof of Theorem simpl

Step	Hyp	Ref	Expression
1		ax-ia1 106	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)

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  2914  rr19.28v  2943  elrab3t  2958  eueq3dc  2977  mosubt  2980  reu6  2992  sbc2iegf  3099  sbcralt  3105  sbcrext  3106  rmob  3122  csbiebt  3164  ssab2  3308  difdif  3329  uneqin  3455  indifdir  3460  undif3ss  3465  rexm  3591  eqifdc  3639  ifandc  3643  ifnebibdc  3648  difsn  3805  opprc1  3879  unissel  3917  ssmin  3942  abssexg  4267  undifexmid  4278  pwntru  4284  exmidundif  4291  exmidundifim  4292  opelopabsb  4349  elopabran  4373  sess1  4429  ordelord  4473  onin  4478  suctr  4513  abnexg  4538  ifexg  4577  ordtriexmidlem  4612  ordtri2or2exmid  4664  ontri2orexmidim  4665  tfi  4675  peano1  4687  peano2  4688  nnpredcl  4716  0nelxp  4748  0nelelxp  4749  brab2a  4774  mosubopt  4786  posng  4793  opabssxp  4795  ideqg  4876  relssres  5046  trin2  5123  dminss  5146  iota4an  5302  iota2  5311  iotam  5313  fununfun  5367  fun11uni  5394  imadiflem  5403  funimaexg  5408  fneq12  5417  fvelrnb  5686  dffo4  5788  ffnfv  5798  ffvresb  5803  fmptco  5806  fcoconst  5811  funopsn  5822  fcof1  5916  isotr  5949  isopolem  5955  f1oiso  5959  acexmidlemcase  6005  ovprc1  6047  fnoprabg  6114  elovmporab  6214  elovmporab1w  6215  uchoice  6292  op1steq  6334  dmmpog  6366  1stconst  6378  f1o2ndf1  6385  brtpos2  6408  tpostpos  6421  tposf12  6426  smores  6449  tfrlemi1  6489  tfr1onlembfn  6501  tfri1dALT  6508  tfrcllembfn  6514  freceq1  6549  freceq2  6550  frectfr  6557  omv2  6624  omsuc  6631  nnsucelsuc  6650  nntri3  6656  nnaordi  6667  nnmordi  6675  nnm00  6689  ecexr  6698  ertr  6708  swoer  6721  erth  6739  ecelqsdm  6765  iinerm  6767  ecinxp  6770  erovlem  6787  pmresg  6836  resixp  6893  elixpsn  6895  mapsnf1o  6897  dom3  6940  mapdom1g  7021  ssenen  7025  phpelm  7041  finexdc  7078  exmidpweq  7087  nnwetri  7094  fiintim  7109  infidc  7117  ssfii  7157  fiss  7160  dcfi  7164  supubti  7182  supisoex  7192  ordiso2  7218  inl11  7248  omp1eomlem  7277  nnnninf  7309  nninfisol  7316  ctssexmid  7333  ismkvnex  7338  omniwomnimkv  7350  nninfwlpor  7357  nninfwlpoim  7362  nninfinfwlpo  7363  en2eleq  7389  en2other2  7390  exmidfodomrlemr  7396  exmidfodomrlemrALT  7397  acnrcl  7399  exmidaclem  7406  djuen  7409  djudoml  7417  netap  7456  2omotaplemst  7460  exmidapne  7462  cc1  7467  acnccim  7474  dmaddpqlem  7580  distrnqg  7590  ltanqi  7605  ltmnqi  7606  ltaddnq  7610  ltrnqg  7623  ltnnnq  7626  enq0sym  7635  addnq0mo  7650  mulnq0mo  7651  addnnnq0  7652  distrnq0  7662  prarloclemn  7702  prarloc  7706  ltdfpr  7709  genplt2i  7713  addnqprl  7732  addnqpru  7733  nqprl  7754  appdivnq  7766  1idprl  7793  1idpru  7794  ltexpri  7816  recexpr  7841  cauappcvgprlemdisj  7854  archrecpr  7867  addsrmo  7946  mulsrmo  7947  addsrpr  7948  mulsrpr  7949  0idsr  7970  1idsr  7971  archsr  7985  prsradd  7989  prsrlt  7990  caucvgsr  8005  map2psrprg  8008  elrealeu  8032  muladd11r  8318  negeu  8353  pncan  8368  pncan3  8370  negsub  8410  addid0  8535  posdif  8618  ltnegcon1  8626  subge0  8638  suble0  8639  lesub0  8642  reapval  8739  reapneg  8760  ap0gt0  8803  aprcl  8809  lt0ap0  8811  recextlem1  8814  recapb  8834  div0ap  8865  recrecap  8872  rec11ap  8873  recgt0  9013  mulgt1  9026  lerec2  9052  recp1lt1  9062  recreclt  9063  ledivp1  9066  negiso  9118  nnsub  9165  avglt1  9366  nnrecl  9383  nnnn0addcl  9415  elnn0nn  9427  nn0ge2m1nn  9445  zaddcl  9502  eluzmn  9745  eluzadd  9768  infregelbex  9810  divfnzn  9833  qaddcl  9847  qreccl  9854  cnref1o  9863  ge0p1rp  9898  divlt1lt  9937  divle1le  9938  addlelt  9981  xrre3  10035  xltnegi  10048  xaddval  10058  xaddcom  10074  xnegdi  10081  xposdif  10095  ixxssixx  10115  iccshftr  10207  iccshftl  10209  iccdil  10211  icccntr  10213  zltaddlt1le  10220  elfz2  10228  peano2fzr  10250  fzdcel  10253  fzsplit2  10263  fzaddel  10272  fzrev2  10298  fzrev2i  10299  fzrev3  10300  elfz1b  10303  fseq1p1m1  10307  uzsubfz0  10342  fzosubel3  10419  eluzgtdifelfzo  10420  fzofzp1b  10451  elfzomelpfzo  10454  exfzdc  10463  fvinim0ffz  10464  zsupcllemex  10467  infssuzcldc  10472  exbtwnzlemshrink  10485  qbtwnz  10488  qbtwnxr  10494  ico0  10498  elicore  10503  xqltnle  10504  apbtwnz  10511  flqge  10519  flqlt  10520  flqltnz  10524  flqbi2  10528  flqaddz  10534  flqmulnn0  10536  intfracq  10559  flqdiv  10560  q0mod  10594  q1mod  10595  mulp1mod1  10604  q2txmodxeq0  10623  modfzo0difsn  10634  frec2uzuzd  10641  frec2uzltd  10642  frec2uzrand  10644  uzennn  10675  seqfveq2g  10716  seq3split  10727  seqsplitg  10728  seq3caopr  10734  seqcaoprg  10735  seqf1oglem2  10759  seqf1og  10760  exp3vallem  10779  exp3val  10780  expnnval  10781  exp1  10784  expcl2lemap  10790  rpexpcl  10797  expnegzap  10812  mulexp  10817  mulexpzap  10818  leexp2r  10832  leexp1a  10833  sq11  10851  subsq  10885  binom2  10890  binom3  10896  zesq  10897  bernneq  10899  sq11ap  10946  zzlesq  10947  mulsubdivbinom2ap  10950  apexp1  10957  facwordi  10979  facubnd  10984  facavg  10985  bcval  10988  bcval5  11002  hashennn  11019  fihashf1rn  11027  fseq1hash  11040  hashdifsn  11059  hashdifpr  11060  hashxp  11066  fiubz  11069  fiubnn  11070  fnfz0hash  11072  ffzo0hash  11074  hash2en  11083  wrdval  11092  ffz0iswrdnn0  11116  wrdsymb0  11122  ccatsymb  11155  ccatval21sw  11158  lswccatn0lsw  11164  ccatalpha  11166  ccatrcl1  11167  s111  11184  ccat1st1st  11193  lswccats1fst  11196  swrdlen2  11215  swrdfv2  11216  swrdsbslen  11219  swrds1  11221  ccatswrd  11223  pfxval  11227  pfxclg  11231  pfxmpt  11233  pfxid  11239  pfxfv0  11245  pfxtrcfv0  11247  pfxfvlsw  11248  pfxeq  11249  ccatpfx  11254  swrdpfx  11260  lenrevpfxcctswrd  11265  wrdeqs1cat  11273  cats1un  11274  swrdccatin1  11278  pfxccatin12lem2a  11280  pfxccatin12lem1  11281  pfxccatin12lem3  11285  pfxccatin12  11286  swrdccat  11288  pfxccat3a  11291  swrdccat3blem  11292  swrdccat3b  11293  reuccatpfxs1lem  11299  reuccatpfxs1  11300  s2cl  11338  s2fv0g  11340  shftfvalg  11350  ovshftex  11351  shftdm  11354  shftfib  11355  shftval  11357  shftf  11362  crre  11389  cjexp  11425  cjreim2  11436  uzin2  11519  rexuz3  11522  resqrexlemgt0  11552  resqrex  11558  sqrtgt0  11566  sqrtsq  11576  sqrtmsq  11577  absrpclap  11593  absext  11595  absmul  11601  absid  11603  absexp  11611  nn0abscl  11617  abslt  11620  absle  11621  recvalap  11629  abstri  11636  caubnd2  11649  qdenre  11734  maxabsle  11736  maxabslemval  11740  maxcl  11742  rexanre  11752  min1inf  11764  minabs  11768  minclpr  11769  mul0inf  11773  mingeb  11774  xrmaxiflemcl  11777  xrnegiso  11794  climconst2  11823  climmpt  11832  climres  11835  climcaucn  11883  sumeq1  11887  summodclem2a  11913  isumz  11921  fisumss  11924  fsumzcl2  11937  sumsnf  11941  isumclim3  11955  fsum2dlemstep  11966  fisumcom2  11970  fsumconst  11986  cvgcmpub  12008  binom  12016  binom1p  12017  binom1dif  12019  bcxmas  12021  divcnv  12029  geo2lim  12048  geoisum  12049  geoisumr  12050  geoisum1  12051  mertenslemi1  12067  mertensabs  12069  prod1dc  12118  fprodconst  12152  fprodcom2fi  12158  efcllem  12191  efcj  12205  efadd  12207  efexp  12214  efgt1p2  12227  tanvalap  12240  tanval2ap  12245  tanval3ap  12246  sinadd  12268  cosadd  12269  dvdsdc  12330  iddvdsexp  12347  dvdsadd  12368  dvds1  12385  odd2np1  12405  oddm1even  12407  m1exp1  12433  divalglemnn  12450  fldivndvdslt  12469  flodddiv4lt  12470  bitsp1  12483  bitsmod  12488  bitsfi  12489  bitscmp  12490  bitsinv1lem  12493  dvdsbnd  12498  gcdnncl  12509  zeqzmulgcd  12512  gcdneg  12524  modgcd  12533  bezoutlemex  12543  bezoutlemeu  12549  dfgcd3  12552  gcdzeq  12564  dvdssq  12573  algrf  12588  eucalgval2  12596  eucalgcvga  12601  lcmval  12606  gcddvdslcm  12616  lcmneg  12617  coprmgcdb  12631  qredeu  12640  divgcdcoprm0  12644  divgcdcoprmex  12645  cncongr1  12646  cncongr2  12647  cncongrcoprm  12649  prmind2  12663  dvdsnprmd  12668  exprmfct  12681  isprm6  12690  pw2dvdslemn  12708  oddpwdclemdc  12716  sqrt2irraplemnn  12722  divnumden  12739  divdenle  12740  nn0sqrtelqelz  12749  phivalfi  12755  crth  12767  eulerth  12776  prmdivdiv  12780  reumodprminv  12797  nnnn0modprm0  12799  nnoddn2prmb  12806  pcval  12840  pcidlem  12867  pcid  12868  pcneg  12869  pc2dvds  12874  pcz  12876  pcprod  12890  prmpwdvds  12899  4sqexercise1  12942  2expltfac  12983  xpct  12988  znnen  12990  ennnfonelemg  12995  ennnfone  13017  ctinfom  13020  ctinf  13022  ssomct  13037  isstruct2im  13063  isstruct2r  13064  setsvalg  13083  setsslnid  13105  ressvalsets  13118  ressex  13119  2strbasg  13174  2stropg  13175  2strbas1g  13177  ressmulrg  13199  ressscag  13237  ressvscag  13238  ressipg  13239  restval  13299  restid2  13302  prdsex  13323  pwsval  13345  qusex  13379  fnpr2o  13393  xpsfval  13402  xpsval  13406  intopsn  13421  mgmidmo  13426  lidrididd  13436  ismnddef  13472  mndinvmod  13499  imasmnd2  13506  ismhm  13515  mhmex  13516  insubm  13539  dfgrp2  13581  grpsubval  13600  grpinvinv  13621  grpsubrcan  13635  grpsubadd  13642  grpaddsubass  13644  grpsubsub4  13647  grppnpcan2  13648  grpnpncan  13649  grpnpncan0  13650  grpnnncan2  13651  dfgrp3m  13653  dfgrp3me  13654  imasgrp2  13668  mhmmnd  13674  mulgfvalg  13679  mulgval  13680  mulgfng  13682  mulg1  13687  mulgnnp1  13688  mulgnndir  13709  mulgass  13717  mulgmodid  13719  issubg2m  13747  grpissubg  13752  isnsg  13760  isnsg3  13765  0nsg  13772  eqgfval  13780  eqger  13782  eqgen  13785  eqgcpbl  13786  quseccl  13791  isghm  13801  kerf1ghm  13832  conjghm  13834  conjsubg  13835  abladdsub  13873  ablpncan3  13875  ablsubsub23  13883  invghm  13887  subgabl  13890  mgpress  13915  rngdi  13924  rnglz  13929  imasrng  13940  srgmulgass  13973  srgrmhm  13978  isring  13984  ringo2times  14012  ringrng  14020  ringlz  14027  imasring  14048  opprrng  14061  opprrngbg  14062  opprring  14063  mulgass3  14069  dvdsrd  14079  dvdsrneg  14088  unitnegcl  14115  dvrvald  14119  dvrid  14122  dvr1  14123  dvrass  14124  dvrdir  14128  ringinvdv  14130  rhmex  14142  isrim0  14146  rhmval  14158  rhmdvdsr  14160  rhmopp  14161  elrhmunit  14162  rhmunitinv  14163  isnzr2  14169  ringelnzr  14172  issubrng2  14195  issubrg2  14226  aprap  14271  lmodvs1  14301  lmod0vs  14306  lmodvs0  14307  lmodvsmmulgdi  14308  lmodfopne  14311  lmodvneg1  14315  lss1  14347  islss3  14364  lsslss  14366  lss1d  14368  lspf  14374  lspsn  14401  lspsnneg  14405  sraval  14422  sraring  14434  qus1  14511  qusrhm  14513  cnfldui  14574  dvdsrzring  14588  mulgghm2  14593  mulgrhm  14594  znval  14621  znf1o  14636  psrbagfi  14658  psrplusgg  14663  mplgrpfi  14691  eltg2b  14749  difopn  14803  ntrcls0  14826  neii1  14842  restbasg  14863  resttopon  14866  restuni2  14872  cnrest2r  14932  tx1cn  14964  txcnp  14966  txcn  14970  txswaphmeo  15016  psmettri  15025  xmeteq0  15054  xmettri  15067  metrtri  15072  ssblex  15126  xmeter  15131  isxms2  15147  cnbl0  15229  cnblcld  15230  reopnap  15241  tgioo  15249  addcncntoplem  15256  expcn  15264  rescncf  15276  cncfcdm  15277  mulc1cncf  15284  cncfcncntop  15288  addccncf  15295  cdivcncfap  15299  negcncf  15300  cnopnap  15306  suplociccex  15320  hoverlt1  15344  hovergt0  15345  dich0  15347  limccl  15354  ellimc3apf  15355  cnplimcim  15362  limccnp2lem  15371  reldvg  15374  dvbsssg  15381  dvcjbr  15403  dvcj  15404  dvfre  15405  dvrecap  15408  dvef  15422  plyaddcl  15449  plymulcl  15450  plysubcl  15451  plyrecj  15458  reeff1olem  15466  pilem3  15478  ptolemy  15519  rplogcl  15574  rpcxpef  15589  cxprec  15605  rpcxproot  15609  rplogb1  15643  logbgt0b  15661  logbgcd1irr  15662  binom4  15674  wilthlem1  15675  sgmnncl  15683  dvdsppwf1o  15684  mersenne  15692  lgslem4  15703  lgsval  15704  lgsval2lem  15710  lgsval4a  15722  lgsdir2lem3  15730  lgsdir2  15733  lgsne0  15738  lgsprme0  15742  lgsmulsqcoprm  15746  gausslemma2dlem0a  15749  gausslemma2dlem1a  15758  2lgslem1b  15789  2lgslem2  15792  2lgsoddprm  15813  struct2slots2dom  15860  structvtxval  15861  structiedg0val  15862  struct2griedg  15868  edgstruct  15885  uhgr0vb  15905  incistruhgr  15911  umgrvad2edg  16030  uspgredg2vlem  16039  uspgredg2v  16040  usgredg2v  16043  ushgredgedg  16045  ushgredgedgloop  16047  usgr0vb  16052  uhgr0vusgr  16057  edg0usgr  16066  vtxdgfval  16074  wksfval  16094  wlkpropg  16096  uspgr2wlkeq2  16138  uspgr2wlkeqi  16139  upgr2wlkdc  16147  clwwlkccatlem  16169  clwwlkng  16174  clwwlkext2edg  16190  clwwlknccat  16191  umgr2cwwkdifex  16193  bj-nnan  16209  bj-indind  16404  bj-omtrans  16428  bj-inf2vnlem1  16442  sscoll2  16460  2omap  16472  pw1map  16474  pwtrufal  16476  sssneq  16481  pw1nct  16482  nninfsellemsuc  16492  nninfomnilem  16498  nnnninfex  16502  exmidsbthrlem  16504  qdencn  16509  trilpo  16525  trirec0  16526  apdiff  16530  iswomninnlem  16531  iswomni0  16533  redcwlpo  16537  redc0  16539  reap0  16540  cndcap  16541  dceqnconst  16542  dcapnconst  16543  neapmkv  16550  neap0mkv  16551