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  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  1505  exsimpl  1641  sbequ2  1793  sbcof2  1834  sbequilem  1862  sbequ8  1871  euan  2111  mooran1  2127  eupickbi  2137  2exeu  2147  dimatis  2172  rexim  2601  r19.26  2633  r19.40  2661  rspcime  2888  rr19.28v  2917  elrab3t  2932  eueq3dc  2951  mosubt  2954  reu6  2966  sbc2iegf  3073  sbcralt  3079  sbcrext  3080  rmob  3095  csbiebt  3137  ssab2  3281  difdif  3302  uneqin  3428  indifdir  3433  undif3ss  3438  rexm  3564  eqifdc  3611  ifandc  3614  ifnebibdc  3619  difsn  3775  opprc1  3846  unissel  3884  ssmin  3909  abssexg  4233  undifexmid  4244  pwntru  4250  exmidundif  4257  exmidundifim  4258  opelopabsb  4313  sess1  4391  ordelord  4435  onin  4440  suctr  4475  abnexg  4500  ifexg  4539  ordtriexmidlem  4574  ordtri2or2exmid  4626  ontri2orexmidim  4627  tfi  4637  peano1  4649  peano2  4650  nnpredcl  4678  0nelxp  4710  0nelelxp  4711  brab2a  4735  mosubopt  4747  posng  4754  opabssxp  4756  ideqg  4836  relssres  5005  trin2  5082  dminss  5105  iota4an  5260  iota2  5269  iotam  5271  fununfun  5325  fun11uni  5352  imadiflem  5361  funimaexg  5366  fneq12  5375  fvelrnb  5638  dffo4  5740  ffnfv  5750  ffvresb  5755  fmptco  5758  fcoconst  5763  funopsn  5774  fcof1  5864  isotr  5897  isopolem  5903  f1oiso  5907  acexmidlemcase  5951  ovprc1  5993  fnoprabg  6058  elovmporab  6158  elovmporab1w  6159  uchoice  6235  op1steq  6277  dmmpog  6307  1stconst  6319  f1o2ndf1  6326  brtpos2  6349  tpostpos  6362  tposf12  6367  smores  6390  tfrlemi1  6430  tfr1onlembfn  6442  tfri1dALT  6449  tfrcllembfn  6455  freceq1  6490  freceq2  6491  frectfr  6498  omv2  6563  omsuc  6570  nnsucelsuc  6589  nntri3  6595  nnaordi  6606  nnmordi  6614  nnm00  6628  ecexr  6637  ertr  6647  swoer  6660  erth  6678  ecelqsdm  6704  iinerm  6706  ecinxp  6709  erovlem  6726  pmresg  6775  resixp  6832  elixpsn  6834  mapsnf1o  6836  dom3  6879  mapdom1g  6958  ssenen  6962  phpelm  6977  finexdc  7013  exmidpweq  7020  nnwetri  7027  fiintim  7042  infidc  7050  ssfii  7090  fiss  7093  dcfi  7097  supubti  7115  supisoex  7125  ordiso2  7151  inl11  7181  omp1eomlem  7210  nnnninf  7242  nninfisol  7249  ctssexmid  7266  ismkvnex  7271  omniwomnimkv  7283  nninfwlpor  7290  nninfwlpoim  7295  nninfinfwlpo  7296  en2eleq  7318  en2other2  7319  exmidfodomrlemr  7325  exmidfodomrlemrALT  7326  acnrcl  7328  exmidaclem  7335  djuen  7338  djudoml  7346  netap  7381  2omotaplemst  7385  exmidapne  7387  cc1  7392  acnccim  7399  dmaddpqlem  7505  distrnqg  7515  ltanqi  7530  ltmnqi  7531  ltaddnq  7535  ltrnqg  7548  ltnnnq  7551  enq0sym  7560  addnq0mo  7575  mulnq0mo  7576  addnnnq0  7577  distrnq0  7587  prarloclemn  7627  prarloc  7631  ltdfpr  7634  genplt2i  7638  addnqprl  7657  addnqpru  7658  nqprl  7679  appdivnq  7691  1idprl  7718  1idpru  7719  ltexpri  7741  recexpr  7766  cauappcvgprlemdisj  7779  archrecpr  7792  addsrmo  7871  mulsrmo  7872  addsrpr  7873  mulsrpr  7874  0idsr  7895  1idsr  7896  archsr  7910  prsradd  7914  prsrlt  7915  caucvgsr  7930  map2psrprg  7933  elrealeu  7957  muladd11r  8243  negeu  8278  pncan  8293  pncan3  8295  negsub  8335  addid0  8460  posdif  8543  ltnegcon1  8551  subge0  8563  suble0  8564  lesub0  8567  reapval  8664  reapneg  8685  ap0gt0  8728  aprcl  8734  lt0ap0  8736  recextlem1  8739  recapb  8759  div0ap  8790  recrecap  8797  rec11ap  8798  recgt0  8938  mulgt1  8951  lerec2  8977  recp1lt1  8987  recreclt  8988  ledivp1  8991  negiso  9043  nnsub  9090  avglt1  9291  nnrecl  9308  nnnn0addcl  9340  elnn0nn  9352  nn0ge2m1nn  9370  zaddcl  9427  eluzadd  9692  infregelbex  9734  divfnzn  9757  qaddcl  9771  qreccl  9778  cnref1o  9787  ge0p1rp  9822  divlt1lt  9861  divle1le  9862  addlelt  9905  xrre3  9959  xltnegi  9972  xaddval  9982  xaddcom  9998  xnegdi  10005  xposdif  10019  ixxssixx  10039  iccshftr  10131  iccshftl  10133  iccdil  10135  icccntr  10137  zltaddlt1le  10144  elfz2  10152  peano2fzr  10174  fzdcel  10177  fzsplit2  10187  fzaddel  10196  fzrev2  10222  fzrev2i  10223  fzrev3  10224  elfz1b  10227  fseq1p1m1  10231  uzsubfz0  10266  fzosubel3  10342  eluzgtdifelfzo  10343  fzofzp1b  10374  elfzomelpfzo  10377  exfzdc  10386  fvinim0ffz  10387  zsupcllemex  10390  infssuzcldc  10395  exbtwnzlemshrink  10408  qbtwnz  10411  qbtwnxr  10417  ico0  10421  elicore  10426  xqltnle  10427  apbtwnz  10434  flqge  10442  flqlt  10443  flqltnz  10447  flqbi2  10451  flqaddz  10457  flqmulnn0  10459  intfracq  10482  flqdiv  10483  q0mod  10517  q1mod  10518  mulp1mod1  10527  q2txmodxeq0  10546  modfzo0difsn  10557  frec2uzuzd  10564  frec2uzltd  10565  frec2uzrand  10567  uzennn  10598  seqfveq2g  10639  seq3split  10650  seqsplitg  10651  seq3caopr  10657  seqcaoprg  10658  seqf1oglem2  10682  seqf1og  10683  exp3vallem  10702  exp3val  10703  expnnval  10704  exp1  10707  expcl2lemap  10713  rpexpcl  10720  expnegzap  10735  mulexp  10740  mulexpzap  10741  leexp2r  10755  leexp1a  10756  sq11  10774  subsq  10808  binom2  10813  binom3  10819  zesq  10820  bernneq  10822  sq11ap  10869  zzlesq  10870  mulsubdivbinom2ap  10873  apexp1  10880  facwordi  10902  facubnd  10907  facavg  10908  bcval  10911  bcval5  10925  hashennn  10942  fihashf1rn  10950  fseq1hash  10963  hashdifsn  10981  hashdifpr  10982  hashxp  10988  fiubz  10991  fiubnn  10992  fnfz0hash  10994  ffzo0hash  10996  hash2en  11005  wrdval  11014  wrdsymb0  11043  ccatsymb  11076  ccatval21sw  11079  lswccatn0lsw  11085  s111  11103  ccat1st1st  11111  lswccats1fst  11114  swrdlen2  11133  swrdfv2  11134  swrdsbslen  11137  swrds1  11139  ccatswrd  11141  pfxval  11145  pfxclg  11149  pfxmpt  11151  pfxid  11157  pfxfv0  11163  pfxtrcfv0  11165  pfxfvlsw  11166  pfxeq  11167  ccatpfx  11172  swrdpfx  11178  lenrevpfxcctswrd  11183  wrdeqs1cat  11191  cats1un  11192  shftfvalg  11199  ovshftex  11200  shftdm  11203  shftfib  11204  shftval  11206  shftf  11211  crre  11238  cjexp  11274  cjreim2  11285  uzin2  11368  rexuz3  11371  resqrexlemgt0  11401  resqrex  11407  sqrtgt0  11415  sqrtsq  11425  sqrtmsq  11426  absrpclap  11442  absext  11444  absmul  11450  absid  11452  absexp  11460  nn0abscl  11466  abslt  11469  absle  11470  recvalap  11478  abstri  11485  caubnd2  11498  qdenre  11583  maxabsle  11585  maxabslemval  11589  maxcl  11591  rexanre  11601  min1inf  11613  minabs  11617  minclpr  11618  mul0inf  11622  mingeb  11623  xrmaxiflemcl  11626  xrnegiso  11643  climconst2  11672  climmpt  11681  climres  11684  climcaucn  11732  sumeq1  11736  summodclem2a  11762  isumz  11770  fisumss  11773  fsumzcl2  11786  sumsnf  11790  isumclim3  11804  fsum2dlemstep  11815  fisumcom2  11819  fsumconst  11835  cvgcmpub  11857  binom  11865  binom1p  11866  binom1dif  11868  bcxmas  11870  divcnv  11878  geo2lim  11897  geoisum  11898  geoisumr  11899  geoisum1  11900  mertenslemi1  11916  mertensabs  11918  prod1dc  11967  fprodconst  12001  fprodcom2fi  12007  efcllem  12040  efcj  12054  efadd  12056  efexp  12063  efgt1p2  12076  tanvalap  12089  tanval2ap  12094  tanval3ap  12095  sinadd  12117  cosadd  12118  dvdsdc  12179  iddvdsexp  12196  dvdsadd  12217  dvds1  12234  odd2np1  12254  oddm1even  12256  m1exp1  12282  divalglemnn  12299  fldivndvdslt  12318  flodddiv4lt  12319  bitsp1  12332  bitsmod  12337  bitsfi  12338  bitscmp  12339  bitsinv1lem  12342  dvdsbnd  12347  gcdnncl  12358  zeqzmulgcd  12361  gcdneg  12373  modgcd  12382  bezoutlemex  12392  bezoutlemeu  12398  dfgcd3  12401  gcdzeq  12413  dvdssq  12422  algrf  12437  eucalgval2  12445  eucalgcvga  12450  lcmval  12455  gcddvdslcm  12465  lcmneg  12466  coprmgcdb  12480  qredeu  12489  divgcdcoprm0  12493  divgcdcoprmex  12494  cncongr1  12495  cncongr2  12496  cncongrcoprm  12498  prmind2  12512  dvdsnprmd  12517  exprmfct  12530  isprm6  12539  pw2dvdslemn  12557  oddpwdclemdc  12565  sqrt2irraplemnn  12571  divnumden  12588  divdenle  12589  nn0sqrtelqelz  12598  phivalfi  12604  crth  12616  eulerth  12625  prmdivdiv  12629  reumodprminv  12646  nnnn0modprm0  12648  nnoddn2prmb  12655  pcval  12689  pcidlem  12716  pcid  12717  pcneg  12718  pc2dvds  12723  pcz  12725  pcprod  12739  prmpwdvds  12748  4sqexercise1  12791  2expltfac  12832  xpct  12837  znnen  12839  ennnfonelemg  12844  ennnfone  12866  ctinfom  12869  ctinf  12871  ssomct  12886  isstruct2im  12912  isstruct2r  12913  setsvalg  12932  setsslnid  12954  ressvalsets  12966  ressex  12967  2strbasg  13022  2stropg  13023  2strbas1g  13025  ressmulrg  13047  ressscag  13085  ressvscag  13086  ressipg  13087  restval  13147  restid2  13150  prdsex  13171  pwsval  13193  qusex  13227  fnpr2o  13241  xpsfval  13250  xpsval  13254  intopsn  13269  mgmidmo  13274  lidrididd  13284  ismnddef  13320  mndinvmod  13347  imasmnd2  13354  ismhm  13363  mhmex  13364  insubm  13387  dfgrp2  13429  grpsubval  13448  grpinvinv  13469  grpsubrcan  13483  grpsubadd  13490  grpaddsubass  13492  grpsubsub4  13495  grppnpcan2  13496  grpnpncan  13497  grpnpncan0  13498  grpnnncan2  13499  dfgrp3m  13501  dfgrp3me  13502  imasgrp2  13516  mhmmnd  13522  mulgfvalg  13527  mulgval  13528  mulgfng  13530  mulg1  13535  mulgnnp1  13536  mulgnndir  13557  mulgass  13565  mulgmodid  13567  issubg2m  13595  grpissubg  13600  isnsg  13608  isnsg3  13613  0nsg  13620  eqgfval  13628  eqger  13630  eqgen  13633  eqgcpbl  13634  quseccl  13639  isghm  13649  kerf1ghm  13680  conjghm  13682  conjsubg  13683  abladdsub  13721  ablpncan3  13723  ablsubsub23  13731  invghm  13735  subgabl  13738  mgpress  13763  rngdi  13772  rnglz  13777  imasrng  13788  srgmulgass  13821  srgrmhm  13826  isring  13832  ringo2times  13860  ringrng  13868  ringlz  13875  imasring  13896  opprrng  13909  opprrngbg  13910  opprring  13911  mulgass3  13917  dvdsrd  13926  dvdsrneg  13935  unitnegcl  13962  dvrvald  13966  dvrid  13969  dvr1  13970  dvrass  13971  dvrdir  13975  ringinvdv  13977  rhmex  13989  isrim0  13993  rhmval  14005  rhmdvdsr  14007  rhmopp  14008  elrhmunit  14009  rhmunitinv  14010  isnzr2  14016  ringelnzr  14019  issubrng2  14042  issubrg2  14073  aprap  14118  lmodvs1  14148  lmod0vs  14153  lmodvs0  14154  lmodvsmmulgdi  14155  lmodfopne  14158  lmodvneg1  14162  lss1  14194  islss3  14211  lsslss  14213  lss1d  14215  lspf  14221  lspsn  14248  lspsnneg  14252  sraval  14269  sraring  14281  qus1  14358  qusrhm  14360  cnfldui  14421  dvdsrzring  14435  mulgghm2  14440  mulgrhm  14441  znval  14468  znf1o  14483  psrbagfi  14505  psrplusgg  14510  mplgrpfi  14538  eltg2b  14596  difopn  14650  ntrcls0  14673  neii1  14689  restbasg  14710  resttopon  14713  restuni2  14719  cnrest2r  14779  tx1cn  14811  txcnp  14813  txcn  14817  txswaphmeo  14863  psmettri  14872  xmeteq0  14901  xmettri  14914  metrtri  14919  ssblex  14973  xmeter  14978  isxms2  14994  cnbl0  15076  cnblcld  15077  reopnap  15088  tgioo  15096  addcncntoplem  15103  expcn  15111  rescncf  15123  cncfcdm  15124  mulc1cncf  15131  cncfcncntop  15135  addccncf  15142  cdivcncfap  15146  negcncf  15147  cnopnap  15153  suplociccex  15167  hoverlt1  15191  hovergt0  15192  dich0  15194  limccl  15201  ellimc3apf  15202  cnplimcim  15209  limccnp2lem  15218  reldvg  15221  dvbsssg  15228  dvcjbr  15250  dvcj  15251  dvfre  15252  dvrecap  15255  dvef  15269  plyaddcl  15296  plymulcl  15297  plysubcl  15298  plyrecj  15305  reeff1olem  15313  pilem3  15325  ptolemy  15366  rplogcl  15421  rpcxpef  15436  cxprec  15452  rpcxproot  15456  rplogb1  15490  logbgt0b  15508  logbgcd1irr  15509  binom4  15521  wilthlem1  15522  sgmnncl  15530  dvdsppwf1o  15531  mersenne  15539  lgslem4  15550  lgsval  15551  lgsval2lem  15557  lgsval4a  15569  lgsdir2lem3  15577  lgsdir2  15580  lgsne0  15585  lgsprme0  15589  lgsmulsqcoprm  15593  gausslemma2dlem0a  15596  gausslemma2dlem1a  15605  2lgslem1b  15636  2lgslem2  15639  2lgsoddprm  15660  struct2slots2dom  15707  structvtxval  15708  structiedg0val  15709  struct2griedg  15715  edgstruct  15730  uhgr0vb  15750  incistruhgr  15756  bj-nnan  15806  bj-indind  16002  bj-omtrans  16026  bj-inf2vnlem1  16040  sscoll2  16058  2omap  16067  pwtrufal  16069  sssneq  16074  pw1nct  16075  nninfsellemsuc  16084  nninfomnilem  16090  nnnninfex  16094  exmidsbthrlem  16096  qdencn  16101  trilpo  16117  trirec0  16118  apdiff  16122  iswomninnlem  16123  iswomni0  16125  redcwlpo  16129  redc0  16131  reap0  16132  cndcap  16133  dceqnconst  16134  dcapnconst  16135  neapmkv  16142  neap0mkv  16143