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  6526  tpostpos  6539  tposf12  6544  smores  6567  tfrlemi1  6607  tfr1onlembfn  6619  tfri1dALT  6626  tfrcllembfn  6632  freceq1  6667  freceq2  6668  frectfr  6675  omv2  6742  omsuc  6749  nnsucelsuc  6768  nntri3  6774  nnaordi  6785  nnmordi  6793  nnm00  6807  ecexr  6816  ertr  6826  swoer  6839  erth  6857  ecelqsdm  6883  iinerm  6885  ecinxp  6888  erovlem  6905  pmresg  6961  resixp  7019  elixpsn  7021  mapsnf1o  7023  dom3  7066  modom  7112  mapdom1g  7151  ssenen  7156  phpelm  7172  finexdc  7211  exmidpweq  7220  nnwetri  7227  fiintim  7242  infidc  7252  suppeqfsuppbi  7300  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  fcdmnn0fsuppg  9629  nn0ge2m1nn  9638  zaddcl  9695  eluzmn  9944  eluzadd  9967  infregelbex  10014  divfnzn  10037  qaddcl  10051  qreccl  10058  cnref1o  10068  ge0p1rp  10103  divlt1lt  10142  divle1le  10143  addlelt  10186  xrre3  10241  xltnegi  10254  xaddval  10264  xaddcom  10280  xnegdi  10287  xposdif  10301  ixxssixx  10321  iccshftr  10413  iccshftl  10415  iccdil  10417  icccntr  10419  zltaddlt1le  10427  elfz2  10435  peano2fzr  10458  fzdcel  10461  fzsplit2  10472  fzaddel  10482  fzrev2  10509  fzrev2i  10510  fzrev3  10511  elfz1b  10514  fseq1p1m1  10518  uzsubfz0  10553  fzosubel3  10631  eluzgtdifelfzo  10632  fzofzp1b  10663  elfzomelpfzo  10666  exfzdc  10676  fvinim0ffz  10677  zsupcllemex  10680  infssuzcldc  10685  exbtwnzlemshrink  10700  qbtwnz  10703  qbtwnxr  10709  ico0  10713  elicore  10718  xqltnle  10719  apbtwnz  10726  flaplelt  10730  flqge  10736  flapge  10737  flqlt  10738  flqltnz  10743  flqbi2  10747  flqaddz  10753  flqmulnn0  10755  intfracq  10778  flqdiv  10779  q0mod  10813  q1mod  10814  mulp1mod1  10823  q2txmodxeq0  10842  modfzo0difsn  10853  frec2uzuzd  10860  frec2uzltd  10861  frec2uzrand  10863  uzennn  10894  seqfveq2g  10935  seq3split  10946  seqsplitg  10947  seq3caopr  10953  seqcaoprg  10954  seqf1oglem2  10978  seqf1og  10979  exp3vallem  10998  exp3val  10999  expnnval  11000  exp1  11003  expcl2lemap  11009  rpexpcl  11016  expnegzap  11031  mulexp  11036  mulexpzap  11037  leexp2r  11051  leexp1a  11052  sq11  11070  subsq  11104  binom2  11109  binom3  11115  zesq  11117  bernneq  11119  sq11ap  11166  zzlesq  11167  mulsubdivbinom2ap  11171  apexp1  11178  facwordi  11200  facubnd  11205  facavg  11206  bcval  11209  bcval5  11223  hashennn  11241  fihashf1rn  11249  fseq1hash  11263  hashdifsn  11282  hashdifpr  11283  hashxp  11289  hashmap  11290  fiubz  11294  fiubnn  11295  fnfz0hash  11297  ffzo0hash  11299  ssenneg  11302  hashfibclem  11304  hashf1  11309  hash2en  11317  wrdval  11329  ffz0iswrdnn0  11353  wrdsymb0  11359  ccatsymb  11392  ccatval21sw  11395  lswccatn0lsw  11401  ccatalpha  11403  ccatrcl1  11404  s111  11421  ccat1st1st  11431  lswccats1fst  11434  swrdlen2  11456  swrdfv2  11457  swrdsbslen  11460  swrds1  11462  ccatswrd  11464  pfxval  11468  pfxclg  11472  pfxmpt  11474  pfxid  11480  pfxfv0  11486  pfxtrcfv0  11488  pfxfvlsw  11489  pfxeq  11490  ccatpfx  11495  swrdpfx  11501  lenrevpfxcctswrd  11506  wrdeqs1cat  11514  cats1un  11515  swrdccatin1  11519  pfxccatin12lem2a  11521  pfxccatin12lem1  11522  pfxccatin12lem3  11526  pfxccatin12  11527  swrdccat  11529  pfxccat3a  11532  swrdccat3blem  11533  swrdccat3b  11534  reuccatpfxs1lem  11540  reuccatpfxs1  11541  s2cl  11579  s2fv0g  11581  shftfvalg  11605  ovshftex  11606  shftdm  11609  shftfib  11610  shftval  11612  shftf  11617  crre  11644  cjexp  11680  cjreim2  11692  uzin2  11775  rexuz3  11778  resqrexlemgt0  11808  resqrex  11814  sqrtgt0  11822  sqrtsq  11832  sqrtmsq  11833  absrpclap  11849  absext  11851  absmul  11857  absid  11859  qabscl  11865  absexp  11868  nn0abscl  11874  abslt  11877  absle  11878  recvalap  11886  abstri  11893  caubnd2  11906  qdenre  11991  maxabsle  11993  maxabslemval  11997  maxcl  11999  rexanre  12009  min1inf  12022  minabs  12026  minclpr  12027  mul0inf  12032  mingeb  12033  xrmaxiflemcl  12036  xrnegiso  12053  climconst2  12082  climmpt  12091  climres  12094  climcaucn  12142  sumeq1  12146  summodclem2a  12173  isumz  12181  fisumss  12184  fsumzcl2  12197  sumsnf  12201  isumclim3  12215  fsum2dlemstep  12226  fisumcom2  12230  fsumconst  12246  cvgcmpub  12268  binom  12276  binom1p  12277  binom1dif  12279  bcxmas  12281  divcnv  12289  geo2lim  12308  geoisum  12309  geoisumr  12310  geoisum1  12311  mertenslemi1  12327  mertensabs  12329  prod1dc  12378  fprodconst  12412  fprodcom2fi  12418  efcllem  12451  efcj  12465  efadd  12467  efexp  12474  efgt1p2  12487  tanvalap  12500  tanval2ap  12505  tanval3ap  12506  sinadd  12528  cosadd  12529  dvdsdc  12590  iddvdsexp  12607  dvdsadd  12628  dvds1  12645  odd2np1  12665  oddm1even  12667  m1exp1  12693  divalglemnn  12710  fldivndvdslt  12729  flodddiv4lt  12730  bitsp1  12743  bitsmod  12748  bitsfi  12749  bitscmp  12750  bitsinv1lem  12753  dvdsbnd  12758  gcdnncl  12769  zeqzmulgcd  12772  gcdneg  12784  modgcd  12793  bezoutlemex  12803  bezoutlemeu  12809  dfgcd3  12812  gcdzeq  12824  dvdssq  12833  algrf  12848  eucalgval2  12856  eucalgcvga  12861  lcmval  12866  gcddvdslcm  12876  lcmneg  12877  coprmgcdb  12891  qredeu  12900  divgcdcoprm0  12904  divgcdcoprmex  12905  cncongr1  12906  cncongr2  12907  cncongrcoprm  12909  prmind2  12923  dvdsnprmd  12928  exprmfct  12942  isprm6  12951  pwbdvds  12970  nnmaxpwlemnfac  12976  nnmaxpwlemparts  12977  nnmaxpw  12978  sqrt2irraplemnn  12984  divnumden  13001  divdenle  13002  nn0sqrtelqelz  13011  phivalfi  13019  crth  13031  eulerth  13040  prmdivdiv  13044  reumodprminv  13061  nnnn0modprm0  13063  nnoddn2prmb  13070  pcval  13104  pcidlem  13131  pcid  13132  pcneg  13133  pc2dvds  13138  pcz  13140  pcprod  13154  prmpwdvds  13163  4sqexercise1  13206  2expltfac  13248  prmlem0  13249  ballotfilemfval  13287  ballotfilemefi  13295  ballotfilemodife  13298  ballotfilem4  13299  ballotfilemsval  13310  ballotfilemieq  13318  ballotfilemrv  13321  ballotfilemrinv0  13334  xpct  13345  znnen  13347  ennnfonelemg  13352  ennnfone  13374  ctinfom  13377  ctinf  13379  ssomct  13394  isstruct2im  13420  isstruct2r  13421  setsvalg  13440  setsslnid  13462  ressvalsets  13476  ressex  13477  2strbasg  13533  2stropg  13534  2strbas1g  13536  ressmulrg  13558  ressscag  13596  ressvscag  13597  ressipg  13598  restval  13658  restid2  13661  qusex  13705  fnpr2o  13719  xpsfval  13728  intopsn  13746  mgmidmo  13751  lidrididd  13761  ismnddef  13790  mndinvmod  13817  imasmnd2  13818  ismhm  13827  mhmex  13828  insubm  13851  dfgrp2  13891  grpsubval  13910  grpinvinv  13931  grpsubrcan  13945  grpsubadd  13952  grpaddsubass  13954  grpsubsub4  13957  grppnpcan2  13958  grpnpncan  13959  grpnpncan0  13960  grpnnncan2  13961  dfgrp3m  13963  dfgrp3me  13964  imasgrp2  13972  mhmmnd  13978  mulgfvalg  13983  mulgval  13984  mulgfng  13986  mulg1  13991  mulgnnp1  13992  mulgnndir  14013  mulgass  14021  mulgmodid  14023  issubg2m  14051  grpissubg  14056  isnsg  14064  isnsg3  14069  0nsg  14076  eqgfval  14084  eqger  14086  eqgen  14089  eqgcpbl  14090  quseccl  14095  isghm  14105  kerf1ghm  14136  conjghm  14138  conjsubg  14139  cntzval  14153  cntzidss  14172  cntrsubgnsg  14175  abladdsub  14209  ablpncan3  14211  ablsubsub23  14219  invghm  14223  subgabl  14226  prdsex  14279  xpsval  14308  pwsval  14311  mgpress  14337  rngdi  14346  rnglz  14351  imasrng  14362  srgmulgass  14400  srgrmhm  14405  isring  14411  ringo2times  14440  ringrng  14448  ringlz  14455  imasring  14478  opprrng  14491  opprrngbg  14492  opprring  14493  mulgass3  14500  dvdsrd  14510  dvdsrneg  14519  unitnegcl  14546  dvrvald  14550  dvrid  14553  dvr1  14554  dvrass  14555  dvrdir  14559  ringinvdv  14561  rhmex  14573  isrim0  14577  rhmval  14589  rhmdvdsr  14591  rhmopp  14592  elrhmunit  14593  rhmunitinv  14594  isnzr2  14600  ringelnzr  14603  issubrng2  14627  issubrg2  14658  ringunitap  14702  aprap  14707  aprnzr  14708  opprdrng  14729  lmodvs1  14762  lmod0vs  14767  lmodvs0  14768  lmodvsmmulgdi  14769  lmodfopne  14772  lmodvneg1  14776  lss1  14808  islss3  14825  lsslss  14827  lss1d  14829  lspf  14835  lspsn  14862  lspsnneg  14866  sraval  14883  sraring  14895  qus1  14972  qusrhm  14974  cnfldui  15033  dvdsrzring  15047  mulgghm2  15052  mulgrhm  15053  znval  15080  znf1o  15095  assa2ass  15118  assa2ass2  15119  issubassa3  15121  assamulgscmlem2  15151  psrbagfi  15168  psrbaglefifi  15172  psrbagconcl  15173  psrplusgg  15182  psrmulrg  15186  mplgrpfi  15222  eltg2b  15280  difopn  15334  ntrcls0  15357  neii1  15373  restbasg  15394  resttopon  15397  restuni2  15403  cnrest2r  15463  tx1cn  15495  txcnp  15497  txcn  15501  txswaphmeo  15547  psmettri  15556  xmeteq0  15585  xmettri  15598  metrtri  15603  ssblex  15657  xmeter  15662  isxms2  15678  cnbl0  15760  cnblcld  15761  reopnap  15772  tgioo  15780  addcncntoplem  15787  expcn  15795  rescncf  15807  cncfcdm  15808  mulc1cncf  15815  cncfcncntop  15819  addccncf  15826  cdivcncfap  15830  negcncf  15831  cnopnap  15837  suplociccex  15851  hoverlt1  15875  hovergt0  15876  dich0  15878  limccl  15885  ellimc3apf  15886  cnplimcim  15893  limccnp2lem  15902  reldvg  15905  dvbsssg  15912  dvcjbr  15934  dvcj  15935  dvfre  15936  dvrecap  15939  dvef  15953  plyaddcl  15980  plymulcl  15981  plysubcl  15982  plyrecj  15989  reeff1olem  15997  pilem3  16010  ptolemy  16051  rplogcl  16109  rpcxpef  16127  cxprec  16143  rpcxproot  16147  rplogb1  16184  logbgt0b  16202  logbgcd1irr  16203  zprmlogbaplem3  16217  binom4  16219  birthdaylem1g  16225  wilthlem1  16232  sgmnncl  16257  ppiprm  16259  dvdsppwf1o  16283  ppiublem1  16291  ppiqub  16293  chtublem  16295  chtqub  16296  mersenne  16297  lgslem4  16327  lgsval  16328  lgsval2lem  16334  lgsval4a  16346  lgsdir2lem3  16354  lgsdir2  16357  lgsne0  16362  lgsprme0  16366  lgsmulsqcoprm  16370  gausslemma2dlem0a  16373  gausslemma2dlem1a  16382  2lgslem1b  16413  2lgslem2  16416  2lgsoddprm  16437  struct2slots2dom  16484  structvtxval  16485  structiedg0val  16486  struct2griedg  16492  edgstruct  16510  uhgr0vb  16530  incistruhgr  16536  umgrvad2edg  16657  uspgredg2vlem  16666  uspgredg2v  16667  usgredg2v  16670  ushgredgedg  16672  ushgredgedgloop  16674  usgr0vb  16679  uhgr0vusgr  16684  edg0usgr  16693  subupgr  16719  upgrspanop  16729  umgrspanop  16730  usgrspanop  16731  vtxdgfval  16734  wksfval  16768  wlkpropg  16770  uspgr2wlkeq2  16812  uspgr2wlkeqi  16813  upgr2wlkdc  16823  trlsex  16833  clwwlkccatlem  16846  clwwlkng  16851  clwwlkext2edg  16868  clwwlknccat  16869  umgr2cwwkdifex  16871  clwwlknonel  16878  clwwlknonccat  16879  clwwlknonex2lem2  16884  clwwlknun  16887  eupthsg  16891  eupth2lem3lem6fi  16917  dichmul0orlem7  16964  dichmul0or  16965  bj-nnan  16969  bj-indind  17163  bj-omtrans  17187  bj-inf2vnlem1  17201  sscoll2  17219  pw1map  17230  pwtrufal  17232  sssneq  17237  pw1nct  17238  exmidnotnotr  17241  idjudju  17252  nninfsellemsuc  17261  nninfomnilem  17267  nnnninfex  17271  exmidsbthrlem  17273  qdencn  17278  trilpo  17299  trirec0  17300  apdiff  17304  iswomninnlem  17306  iswomni0  17308  redcwlpo  17312  redc0  17314  reap0  17315  cndcap  17316  dceqnconst  17317  dcapnconst  17318  neapmkv  17325  neap0mkv  17326  als-no-surprise  17354