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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-ia1 106

This theorem is used by:  simpli  111  simpld  112  imp  124  adantrd  279  iba  300  pm3.41  331  pm4.45im  334  anim12  344  pm4.71  393  adantlr  481  adantrr  483  adantllr  485  adantlrr  487  adantrlr  489  adantrrr  491  simplll  539  simplrl  541  simprll  543  simprrl  545  anabs1  578  jcab  611  pm4.38  613  pm5.21  707  ioran  764  pm3.14  765  pm4.44  791  ordi  828  pm4.39  834  animorl  835  animorlr  837  pm5.16  840  pm5.54dc  930  intnanr  942  intnanrd  944  dcan  946  dedlema  982  dedlemb  983  pm4.42r  984  prlem2  987  ifpdc  992  dfifp2dc  994  simp1l  1052  simp2l  1054  simp3l  1056  3anandis  1388  xordc1  1442  anxordi  1449  falantru  1452  19.26  1534  exsimpl  1670  sbequ2  1822  sbcof2  1863  sbequilem  1891  sbequ8  1900  euan  2143  mooran1  2159  eupickbi  2169  2exeu  2179  dimatis  2204  rexim  2644  r19.26  2677  r19.40  2705  rspcime  2937  rr19.28v  2966  elrab3t  2981  eueq3dc  3000  mosubt  3003  reu6  3015  sbc2iegf  3122  sbcralt  3128  sbcrext  3129  rmob  3145  csbiebt  3187  ssab2  3332  difdif  3354  uneqin  3482  indifdir  3487  undif3ss  3492  abanssl  3501  rexm  3627  eqifdc  3677  ifandc  3681  ifnebibdc  3686  difsn  3852  opprc1  3926  unissel  3964  ssmin  3989  abssexg  4321  undifexmid  4332  pwntru  4338  exmidundif  4345  exmidundifim  4346  opelopabsb  4404  elopabran  4428  sess1  4484  ordelord  4528  onin  4533  suctr  4568  abnexg  4594  ifexg  4633  ordtriexmidlem  4668  ordtri2or2exmid  4720  ontri2orexmidim  4721  tfi  4731  peano1  4743  peano2  4744  nnpredcl  4772  0nelxp  4804  0nelelxp  4805  brab2a  4830  mosubopt  4842  posng  4849  opabssxp  4851  ideqg  4933  relssres  5103  trin2  5182  dminss  5205  iota4an  5361  iota2  5370  iotam  5372  fununfun  5427  fun11uni  5454  imadiflem  5463  funimaexg  5468  fneq12  5477  fvelrnb  5753  dffo4  5859  ffnfv  5869  ffvresb  5874  fmptco  5877  fcoconst  5882  funopsn  5894  fndmexb  5941  mptmex  5948  fcof1  5992  isotr  6025  isopolem  6031  f1oiso  6035  acexmidlemcase  6083  ovprc1  6125  fnoprabg  6192  elovmporab  6292  elovmporab1w  6293  uchoice  6375  op1steq  6417  dmmpog  6449  1stconst  6461  f1o2ndf1  6468  suppfnss  6501  suppssfvg  6507  brtpos2  6527  tpostpos  6540  tposf12  6545  smores  6568  tfrlemi1  6608  tfr1onlembfn  6620  tfri1dALT  6627  tfrcllembfn  6633  freceq1  6668  freceq2  6669  frectfr  6676  omv2  6743  omsuc  6750  nnsucelsuc  6769  nntri3  6775  nnaordi  6786  nnmordi  6794  nnm00  6808  ecexr  6817  ertr  6827  swoer  6840  erth  6858  ecelqsdm  6884  iinerm  6886  ecinxp  6889  erovlem  6906  pmresg  6962  resixp  7021  elixpsn  7023  mapsnf1o  7025  dom3  7068  modom  7114  mapdom1g  7153  ssenen  7158  phpelm  7174  finexdc  7213  exmidpweq  7222  nnwetri  7229  fiintim  7244  infidc  7254  isfsuppfi  7296  ssfii  7313  fiss  7316  dcfi  7320  2omap  7324  supubti  7345  supisoex  7355  ordiso2  7381  inl11  7411  omp1eomlem  7440  nnnninf  7472  nninfisol  7479  ctssexmid  7496  ismkvnex  7501  omniwomnimkv  7513  nninfwlpor  7520  nninfwlpoim  7525  nninfinfwlpo  7526  en2eleq  7553  en2other2  7554  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  acnrcl  7563  exmidaclem  7570  djuen  7573  djudoml  7581  netap  7626  2omotaplemst  7630  exmidapne  7632  cc1  7637  acnccim  7644  dmaddpqlem  7750  distrnqg  7760  ltanqi  7775  ltmnqi  7776  ltaddnq  7780  ltrnqg  7793  ltnnnq  7796  enq0sym  7805  addnq0mo  7820  mulnq0mo  7821  addnnnq0  7822  distrnq0  7832  prarloclemn  7872  prarloc  7876  ltdfpr  7879  genplt2i  7883  addnqprl  7902  addnqpru  7903  nqprl  7924  appdivnq  7936  1idprl  7963  1idpru  7964  ltexpri  7986  recexpr  8011  cauappcvgprlemdisj  8024  archrecpr  8037  addsrmo  8116  mulsrmo  8117  addsrpr  8118  mulsrpr  8119  0idsr  8140  1idsr  8141  archsr  8155  prsradd  8159  prsrlt  8160  caucvgsr  8175  map2psrprg  8178  elrealeu  8202  muladd11r  8489  negeu  8524  pncan  8539  pncan3  8541  negsub  8581  addid0  8706  addeq0  8710  posdif  8790  ltnegcon1  8798  subge0  8810  suble0  8811  lesub0  8814  reapval  8912  reapneg  8933  ap0gt0  8976  aprcl  8982  lt0ap0  8984  recextlem1  8987  recapb  9009  div0ap  9040  recrecap  9047  rec11ap  9048  recgt0  9188  mulgt1  9201  lerec2  9227  recp1lt1  9237  recreclt  9238  ledivp1  9241  negiso  9293  nnsub  9352  avglt1  9555  nnrecl  9572  nnnn0addcl  9604  elnn0nn  9616  nn0ge2m1nn  9636  zaddcl  9693  fcdmnn0fsuppfi  9743  eluzmn  9943  eluzadd  9966  infregelbex  10013  divfnzn  10036  qaddcl  10050  qreccl  10057  cnref1o  10067  ge0p1rp  10102  divlt1lt  10141  divle1le  10142  addlelt  10185  xrre3  10240  xltnegi  10253  xaddval  10263  xaddcom  10279  xnegdi  10286  xposdif  10300  ixxssixx  10320  iccshftr  10412  iccshftl  10414  iccdil  10416  icccntr  10418  zltaddlt1le  10426  elfz2  10434  peano2fzr  10457  fzdcel  10460  fzsplit2  10471  fzaddel  10481  fzrev2  10508  fzrev2i  10509  fzrev3  10510  elfz1b  10513  fseq1p1m1  10517  uzsubfz0  10552  fzosubel3  10630  eluzgtdifelfzo  10631  fzofzp1b  10662  elfzomelpfzo  10665  exfzdc  10675  fvinim0ffz  10676  zsupcllemex  10679  infssuzcldc  10684  exbtwnzlemshrink  10699  qbtwnz  10702  qbtwnxr  10708  ico0  10712  elicore  10717  xqltnle  10718  apbtwnz  10725  flaplelt  10729  flqge  10735  flapge  10736  flqlt  10737  flqltnz  10742  flqbi2  10746  flqaddz  10752  flqmulnn0  10754  intfracq  10777  flqdiv  10778  q0mod  10812  q1mod  10813  mulp1mod1  10822  q2txmodxeq0  10841  modfzo0difsn  10852  frec2uzuzd  10859  frec2uzltd  10860  frec2uzrand  10862  uzennn  10893  seqfveq2g  10934  seq3split  10945  seqsplitg  10946  seq3caopr  10952  seqcaoprg  10953  seqf1oglem2  10977  seqf1og  10978  exp3vallem  10997  exp3val  10998  expnnval  10999  exp1  11002  expcl2lemap  11008  rpexpcl  11015  expnegzap  11030  mulexp  11035  mulexpzap  11036  leexp2r  11050  leexp1a  11051  sq11  11069  subsq  11103  binom2  11108  binom3  11114  zesq  11116  bernneq  11118  sq11ap  11165  zzlesq  11166  mulsubdivbinom2ap  11170  apexp1  11177  facwordi  11199  facubnd  11204  facavg  11205  bcval  11208  bcval5  11222  hashennn  11240  fihashf1rn  11248  fseq1hash  11262  hashdifsn  11281  hashdifpr  11282  hashxp  11288  hashmap  11289  fiubz  11293  fiubnn  11294  fnfz0hash  11296  ffzo0hash  11298  ssenneg  11301  hashfibclem  11303  hashf1  11308  hash2en  11316  wrdval  11328  ffz0iswrdnn0  11352  wrdsymb0  11358  ccatsymb  11391  ccatval21sw  11394  lswccatn0lsw  11400  ccatalpha  11402  ccatrcl1  11403  s111  11420  ccat1st1st  11430  lswccats1fst  11433  swrdlen2  11455  swrdfv2  11456  swrdsbslen  11459  swrds1  11461  ccatswrd  11463  pfxval  11467  pfxclg  11471  pfxmpt  11473  pfxid  11479  pfxfv0  11485  pfxtrcfv0  11487  pfxfvlsw  11488  pfxeq  11489  ccatpfx  11494  swrdpfx  11500  lenrevpfxcctswrd  11505  wrdeqs1cat  11513  cats1un  11514  swrdccatin1  11518  pfxccatin12lem2a  11520  pfxccatin12lem1  11521  pfxccatin12lem3  11525  pfxccatin12  11526  swrdccat  11528  pfxccat3a  11531  swrdccat3blem  11532  swrdccat3b  11533  reuccatpfxs1lem  11539  reuccatpfxs1  11540  s2cl  11578  s2fv0g  11580  shftfvalg  11604  ovshftex  11605  shftdm  11608  shftfib  11609  shftval  11611  shftf  11616  crre  11643  cjexp  11679  cjreim2  11691  uzin2  11774  rexuz3  11777  resqrexlemgt0  11807  resqrex  11813  sqrtgt0  11821  sqrtsq  11831  sqrtmsq  11832  absrpclap  11848  absext  11850  absmul  11856  absid  11858  qabscl  11864  absexp  11867  nn0abscl  11873  abslt  11876  absle  11877  recvalap  11885  abstri  11892  caubnd2  11905  qdenre  11990  maxabsle  11992  maxabslemval  11996  maxcl  11998  rexanre  12008  min1inf  12021  minabs  12025  minclpr  12026  mul0inf  12031  mingeb  12032  xrmaxiflemcl  12035  xrnegiso  12052  climconst2  12081  climmpt  12090  climres  12093  climcaucn  12141  sumeq1  12145  summodclem2a  12172  isumz  12180  fisumss  12183  fsumzcl2  12196  sumsnf  12200  isumclim3  12214  fsum2dlemstep  12225  fisumcom2  12229  fsumconst  12245  cvgcmpub  12267  binom  12275  binom1p  12276  binom1dif  12278  bcxmas  12280  divcnv  12288  geo2lim  12307  geoisum  12308  geoisumr  12309  geoisum1  12310  mertenslemi1  12326  mertensabs  12328  prod1dc  12377  fprodconst  12411  fprodcom2fi  12417  efcllem  12450  efcj  12464  efadd  12466  efexp  12473  efgt1p2  12486  tanvalap  12499  tanval2ap  12504  tanval3ap  12505  sinadd  12527  cosadd  12528  dvdsdc  12589  iddvdsexp  12606  dvdsadd  12627  dvds1  12644  odd2np1  12664  oddm1even  12666  m1exp1  12692  divalglemnn  12709  fldivndvdslt  12728  flodddiv4lt  12729  bitsp1  12742  bitsmod  12747  bitsfi  12748  bitscmp  12749  bitsinv1lem  12752  dvdsbnd  12757  gcdnncl  12768  zeqzmulgcd  12771  gcdneg  12783  modgcd  12792  bezoutlemex  12802  bezoutlemeu  12808  dfgcd3  12811  gcdzeq  12823  dvdssq  12832  algrf  12847  eucalgval2  12855  eucalgcvga  12860  lcmval  12865  gcddvdslcm  12875  lcmneg  12876  coprmgcdb  12890  qredeu  12899  divgcdcoprm0  12903  divgcdcoprmex  12904  cncongr1  12905  cncongr2  12906  cncongrcoprm  12908  prmind2  12922  dvdsnprmd  12927  exprmfct  12941  isprm6  12950  pwbdvds  12969  nnmaxpwlemnfac  12975  nnmaxpwlemparts  12976  nnmaxpw  12977  sqrt2irraplemnn  12983  divnumden  13000  divdenle  13001  nn0sqrtelqelz  13010  phivalfi  13018  crth  13030  eulerth  13039  prmdivdiv  13043  reumodprminv  13060  nnnn0modprm0  13062  nnoddn2prmb  13069  pcval  13103  pcidlem  13130  pcid  13131  pcneg  13132  pc2dvds  13137  pcz  13139  pcprod  13153  prmpwdvds  13162  4sqexercise1  13205  2expltfac  13247  prmlem0  13248  ballotfilemfval  13286  ballotfilemefi  13294  ballotfilemodife  13297  ballotfilem4  13298  ballotfilemsval  13309  ballotfilemieq  13317  ballotfilemrv  13320  ballotfilemrinv0  13333  xpct  13344  znnen  13346  ennnfonelemg  13351  ennnfone  13373  ctinfom  13376  ctinf  13378  ssomct  13393  isstruct2im  13419  isstruct2r  13420  setsvalg  13439  setsslnid  13461  ressvalsets  13475  ressex  13476  2strbasg  13532  2stropg  13533  2strbas1g  13535  ressmulrg  13557  ressscag  13595  ressvscag  13596  ressipg  13597  restval  13657  restid2  13660  qusex  13704  fnpr2o  13718  xpsfval  13727  intopsn  13745  mgmidmo  13750  lidrididd  13760  ismnddef  13789  mndinvmod  13816  imasmnd2  13817  ismhm  13826  mhmex  13827  insubm  13850  dfgrp2  13890  grpsubval  13909  grpinvinv  13930  grpsubrcan  13944  grpsubadd  13951  grpaddsubass  13953  grpsubsub4  13956  grppnpcan2  13957  grpnpncan  13958  grpnpncan0  13959  grpnnncan2  13960  dfgrp3m  13962  dfgrp3me  13963  imasgrp2  13971  mhmmnd  13977  mulgfvalg  13982  mulgval  13983  mulgfng  13985  mulg1  13990  mulgnnp1  13991  mulgnndir  14012  mulgass  14020  mulgmodid  14022  issubg2m  14050  grpissubg  14055  isnsg  14063  isnsg3  14068  0nsg  14075  eqgfval  14083  eqger  14085  eqgen  14088  eqgcpbl  14089  quseccl  14094  isghm  14104  kerf1ghm  14135  conjghm  14137  conjsubg  14138  cntzval  14152  cntzidss  14171  cntrsubgnsg  14174  abladdsub  14208  ablpncan3  14210  ablsubsub23  14218  invghm  14222  subgabl  14225  prdsex  14278  xpsval  14307  pwsval  14310  mgpress  14336  rngdi  14345  rnglz  14350  imasrng  14361  srgmulgass  14399  srgrmhm  14404  isring  14410  ringo2times  14439  ringrng  14447  ringlz  14454  imasring  14477  opprrng  14490  opprrngbg  14491  opprring  14492  mulgass3  14499  dvdsrd  14509  dvdsrneg  14518  unitnegcl  14545  dvrvald  14549  dvrid  14552  dvr1  14553  dvrass  14554  dvrdir  14558  ringinvdv  14560  rhmex  14572  isrim0  14576  rhmval  14588  rhmdvdsr  14590  rhmopp  14591  elrhmunit  14592  rhmunitinv  14593  isnzr2  14599  ringelnzr  14602  issubrng2  14626  issubrg2  14657  ringunitap  14701  aprap  14706  aprnzr  14707  opprdrng  14728  lmodvs1  14761  lmod0vs  14766  lmodvs0  14767  lmodvsmmulgdi  14768  lmodfopne  14771  lmodvneg1  14775  lss1  14807  islss3  14824  lsslss  14826  lss1d  14828  lspf  14834  lspsn  14861  lspsnneg  14865  sraval  14882  sraring  14894  qus1  14971  qusrhm  14973  cnfldui  15032  dvdsrzring  15046  mulgghm2  15051  mulgrhm  15052  znval  15079  znf1o  15094  assa2ass  15117  assa2ass2  15118  issubassa3  15120  assamulgscmlem2  15150  psrbagfi  15166  psrbaglefifi  15175  psrbagconcl  15176  psrplusgg  15191  psrmulrg  15195  mvrfval  15214  mplgrpfi  15239  eltg2b  15297  difopn  15351  ntrcls0  15374  neii1  15390  restbasg  15411  resttopon  15414  restuni2  15420  cnrest2r  15480  tx1cn  15512  txcnp  15514  txcn  15518  txswaphmeo  15564  psmettri  15573  xmeteq0  15602  xmettri  15615  metrtri  15620  ssblex  15674  xmeter  15679  isxms2  15695  cnbl0  15777  cnblcld  15778  reopnap  15789  tgioo  15797  addcncntoplem  15804  expcn  15812  rescncf  15824  cncfcdm  15825  mulc1cncf  15832  cncfcncntop  15836  addccncf  15843  cdivcncfap  15847  negcncf  15848  cnopnap  15854  suplociccex  15868  hoverlt1  15892  hovergt0  15893  dich0  15895  limccl  15902  ellimc3apf  15903  cnplimcim  15910  limccnp2lem  15919  reldvg  15922  dvbsssg  15929  dvcjbr  15951  dvcj  15952  dvfre  15953  dvrecap  15956  dvef  15970  plyaddcl  15997  plymulcl  15998  plysubcl  15999  plyrecj  16006  reeff1olem  16014  pilem3  16027  ptolemy  16068  rplogcl  16126  rpcxpef  16144  cxprec  16160  rpcxproot  16164  rplogb1  16201  logbgt0b  16219  logbgcd1irr  16220  zprmlogbaplem3  16234  binom4  16236  birthdaylem1g  16242  wilthlem1  16249  sgmnncl  16274  ppiprm  16276  dvdsppwf1o  16300  ppiublem1  16308  ppiqub  16310  chtublem  16312  chtqub  16313  mersenne  16314  lgslem4  16344  lgsval  16345  lgsval2lem  16351  lgsval4a  16363  lgsdir2lem3  16371  lgsdir2  16374  lgsne0  16379  lgsprme0  16383  lgsmulsqcoprm  16387  gausslemma2dlem0a  16390  gausslemma2dlem1a  16399  2lgslem1b  16430  2lgslem2  16433  2lgsoddprm  16454  struct2slots2dom  16501  structvtxval  16502  structiedg0val  16503  struct2griedg  16509  edgstruct  16527  uhgr0vb  16547  incistruhgr  16553  umgrvad2edg  16674  uspgredg2vlem  16683  uspgredg2v  16684  usgredg2v  16687  ushgredgedg  16689  ushgredgedgloop  16691  usgr0vb  16696  uhgr0vusgr  16701  edg0usgr  16710  subupgr  16736  upgrspanop  16746  umgrspanop  16747  usgrspanop  16748  vtxdgfval  16751  wksfval  16785  wlkpropg  16787  uspgr2wlkeq2  16829  uspgr2wlkeqi  16830  upgr2wlkdc  16840  trlsex  16850  clwwlkccatlem  16863  clwwlkng  16868  clwwlkext2edg  16885  clwwlknccat  16886  umgr2cwwkdifex  16888  clwwlknonel  16895  clwwlknonccat  16896  clwwlknonex2lem2  16901  clwwlknun  16904  eupthsg  16908  eupth2lem3lem6fi  16934  dichmul0orlem7  16981  dichmul0or  16982  bj-nnan  16986  bj-indind  17180  bj-omtrans  17204  bj-inf2vnlem1  17218  sscoll2  17236  pw1map  17247  pwtrufal  17249  sssneq  17254  pw1nct  17255  exmidnotnotr  17258  idjudju  17269  nninfsellemsuc  17278  nninfomnilem  17284  nnnninfex  17288  exmidsbthrlem  17290  qdencn  17295  trilpo  17316  trirec0  17317  apdiff  17321  iswomninnlem  17323  iswomni0  17325  redcwlpo  17329  redc0  17331  reap0  17332  cndcap  17333  dceqnconst  17334  dcapnconst  17335  neapmkv  17342  neap0mkv  17343  als-no-surprise  17371