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  696  ioran  753  pm3.14  754  pm4.44  780  ordi  817  pm4.39  823  animorl  824  animorlr  826  pm5.16  829  pm5.54dc  919  intnanr  931  intnanrd  933  dcan  935  dedlema  971  dedlemb  972  pm4.42r  973  prlem2  976  simp1l  1023  simp2l  1025  simp3l  1027  3anandis  1358  xordc1  1404  anxordi  1411  falantru  1414  19.26  1495  exsimpl  1631  sbequ2  1783  sbcof2  1824  sbequilem  1852  sbequ8  1861  euan  2101  mooran1  2117  eupickbi  2127  2exeu  2137  dimatis  2162  rexim  2591  r19.26  2623  r19.40  2651  rspcime  2875  rr19.28v  2904  elrab3t  2919  eueq3dc  2938  mosubt  2941  reu6  2953  sbc2iegf  3060  sbcralt  3066  sbcrext  3067  rmob  3082  csbiebt  3124  ssab2  3268  difdif  3289  uneqin  3415  indifdir  3420  undif3ss  3425  rexm  3551  eqifdc  3597  ifandc  3600  ifnebibdc  3605  difsn  3760  opprc1  3831  unissel  3869  ssmin  3894  abssexg  4216  undifexmid  4227  pwntru  4233  exmidundif  4240  exmidundifim  4241  opelopabsb  4295  sess1  4373  ordelord  4417  onin  4422  suctr  4457  abnexg  4482  ifexg  4521  ordtriexmidlem  4556  ordtri2or2exmid  4608  ontri2orexmidim  4609  tfi  4619  peano1  4631  peano2  4632  nnpredcl  4660  0nelxp  4692  0nelelxp  4693  brab2a  4717  mosubopt  4729  posng  4736  opabssxp  4738  ideqg  4818  relssres  4985  trin2  5062  dminss  5085  iota4an  5240  iota2  5249  iotam  5251  fun11uni  5329  imadiflem  5338  funimaexg  5343  fneq12  5352  fvelrnb  5611  dffo4  5713  ffnfv  5723  ffvresb  5728  fmptco  5731  fcoconst  5736  fcof1  5833  isotr  5866  isopolem  5872  f1oiso  5876  acexmidlemcase  5920  ovprc1  5962  fnoprabg  6027  elovmporab  6127  elovmporab1w  6128  uchoice  6204  op1steq  6246  dmmpog  6276  1stconst  6288  f1o2ndf1  6295  brtpos2  6318  tpostpos  6331  tposf12  6336  smores  6359  tfrlemi1  6399  tfr1onlembfn  6411  tfri1dALT  6418  tfrcllembfn  6424  freceq1  6459  freceq2  6460  frectfr  6467  omv2  6532  omsuc  6539  nnsucelsuc  6558  nntri3  6564  nnaordi  6575  nnmordi  6583  nnm00  6597  ecexr  6606  ertr  6616  swoer  6629  erth  6647  ecelqsdm  6673  iinerm  6675  ecinxp  6678  erovlem  6695  pmresg  6744  resixp  6801  elixpsn  6803  mapsnf1o  6805  dom3  6844  mapdom1g  6917  ssenen  6921  phpelm  6936  finexdc  6972  exmidpweq  6979  nnwetri  6986  fiintim  7001  infidc  7009  ssfii  7049  fiss  7052  dcfi  7056  supubti  7074  supisoex  7084  ordiso2  7110  inl11  7140  omp1eomlem  7169  nnnninf  7201  nninfisol  7208  ctssexmid  7225  ismkvnex  7230  omniwomnimkv  7242  nninfwlpor  7249  nninfwlpoim  7254  nninfinfwlpo  7255  en2eleq  7276  en2other2  7277  exmidfodomrlemr  7283  exmidfodomrlemrALT  7284  acnrcl  7286  exmidaclem  7293  djuen  7296  djudoml  7304  netap  7339  2omotaplemst  7343  exmidapne  7345  cc1  7350  acnccim  7357  dmaddpqlem  7463  distrnqg  7473  ltanqi  7488  ltmnqi  7489  ltaddnq  7493  ltrnqg  7506  ltnnnq  7509  enq0sym  7518  addnq0mo  7533  mulnq0mo  7534  addnnnq0  7535  distrnq0  7545  prarloclemn  7585  prarloc  7589  ltdfpr  7592  genplt2i  7596  addnqprl  7615  addnqpru  7616  nqprl  7637  appdivnq  7649  1idprl  7676  1idpru  7677  ltexpri  7699  recexpr  7724  cauappcvgprlemdisj  7737  archrecpr  7750  addsrmo  7829  mulsrmo  7830  addsrpr  7831  mulsrpr  7832  0idsr  7853  1idsr  7854  archsr  7868  prsradd  7872  prsrlt  7873  caucvgsr  7888  map2psrprg  7891  elrealeu  7915  muladd11r  8201  negeu  8236  pncan  8251  pncan3  8253  negsub  8293  addid0  8418  posdif  8501  ltnegcon1  8509  subge0  8521  suble0  8522  lesub0  8525  reapval  8622  reapneg  8643  ap0gt0  8686  aprcl  8692  lt0ap0  8694  recextlem1  8697  recapb  8717  div0ap  8748  recrecap  8755  rec11ap  8756  recgt0  8896  mulgt1  8909  lerec2  8935  recp1lt1  8945  recreclt  8946  ledivp1  8949  negiso  9001  nnsub  9048  avglt1  9249  nnrecl  9266  nnnn0addcl  9298  elnn0nn  9310  nn0ge2m1nn  9328  zaddcl  9385  eluzadd  9649  infregelbex  9691  divfnzn  9714  qaddcl  9728  qreccl  9735  cnref1o  9744  ge0p1rp  9779  divlt1lt  9818  divle1le  9819  addlelt  9862  xrre3  9916  xltnegi  9929  xaddval  9939  xaddcom  9955  xnegdi  9962  xposdif  9976  ixxssixx  9996  iccshftr  10088  iccshftl  10090  iccdil  10092  icccntr  10094  zltaddlt1le  10101  elfz2  10109  peano2fzr  10131  fzdcel  10134  fzsplit2  10144  fzaddel  10153  fzrev2  10179  fzrev2i  10180  fzrev3  10181  elfz1b  10184  fseq1p1m1  10188  uzsubfz0  10223  fzosubel3  10291  eluzgtdifelfzo  10292  fzofzp1b  10323  elfzomelpfzo  10326  exfzdc  10335  fvinim0ffz  10336  zsupcllemex  10339  infssuzcldc  10344  exbtwnzlemshrink  10357  qbtwnz  10360  qbtwnxr  10366  ico0  10370  elicore  10375  xqltnle  10376  apbtwnz  10383  flqge  10391  flqlt  10392  flqltnz  10396  flqbi2  10400  flqaddz  10406  flqmulnn0  10408  intfracq  10431  flqdiv  10432  q0mod  10466  q1mod  10467  mulp1mod1  10476  q2txmodxeq0  10495  modfzo0difsn  10506  frec2uzuzd  10513  frec2uzltd  10514  frec2uzrand  10516  uzennn  10547  seqfveq2g  10588  seq3split  10599  seqsplitg  10600  seq3caopr  10606  seqcaoprg  10607  seqf1oglem2  10631  seqf1og  10632  exp3vallem  10651  exp3val  10652  expnnval  10653  exp1  10656  expcl2lemap  10662  rpexpcl  10669  expnegzap  10684  mulexp  10689  mulexpzap  10690  leexp2r  10704  leexp1a  10705  sq11  10723  subsq  10757  binom2  10762  binom3  10768  zesq  10769  bernneq  10771  sq11ap  10818  zzlesq  10819  mulsubdivbinom2ap  10822  apexp1  10829  facwordi  10851  facubnd  10856  facavg  10857  bcval  10860  bcval5  10874  hashennn  10891  fihashf1rn  10899  fseq1hash  10912  hashdifsn  10930  hashdifpr  10931  hashxp  10937  fiubz  10940  fiubnn  10941  fnfz0hash  10943  ffzo0hash  10945  wrdval  10957  wrdsymb0  10986  shftfvalg  11002  ovshftex  11003  shftdm  11006  shftfib  11007  shftval  11009  shftf  11014  crre  11041  cjexp  11077  cjreim2  11088  uzin2  11171  rexuz3  11174  resqrexlemgt0  11204  resqrex  11210  sqrtgt0  11218  sqrtsq  11228  sqrtmsq  11229  absrpclap  11245  absext  11247  absmul  11253  absid  11255  absexp  11263  nn0abscl  11269  abslt  11272  absle  11273  recvalap  11281  abstri  11288  caubnd2  11301  qdenre  11386  maxabsle  11388  maxabslemval  11392  maxcl  11394  rexanre  11404  min1inf  11416  minabs  11420  minclpr  11421  mul0inf  11425  mingeb  11426  xrmaxiflemcl  11429  xrnegiso  11446  climconst2  11475  climmpt  11484  climres  11487  climcaucn  11535  sumeq1  11539  summodclem2a  11565  isumz  11573  fisumss  11576  fsumzcl2  11589  sumsnf  11593  isumclim3  11607  fsum2dlemstep  11618  fisumcom2  11622  fsumconst  11638  cvgcmpub  11660  binom  11668  binom1p  11669  binom1dif  11671  bcxmas  11673  divcnv  11681  geo2lim  11700  geoisum  11701  geoisumr  11702  geoisum1  11703  mertenslemi1  11719  mertensabs  11721  prod1dc  11770  fprodconst  11804  fprodcom2fi  11810  efcllem  11843  efcj  11857  efadd  11859  efexp  11866  efgt1p2  11879  tanvalap  11892  tanval2ap  11897  tanval3ap  11898  sinadd  11920  cosadd  11921  dvdsdc  11982  iddvdsexp  11999  dvdsadd  12020  dvds1  12037  odd2np1  12057  oddm1even  12059  m1exp1  12085  divalglemnn  12102  fldivndvdslt  12121  flodddiv4lt  12122  bitsp1  12135  bitsmod  12140  bitsfi  12141  bitscmp  12142  bitsinv1lem  12145  dvdsbnd  12150  gcdnncl  12161  zeqzmulgcd  12164  gcdneg  12176  modgcd  12185  bezoutlemex  12195  bezoutlemeu  12201  dfgcd3  12204  gcdzeq  12216  dvdssq  12225  algrf  12240  eucalgval2  12248  eucalgcvga  12253  lcmval  12258  gcddvdslcm  12268  lcmneg  12269  coprmgcdb  12283  qredeu  12292  divgcdcoprm0  12296  divgcdcoprmex  12297  cncongr1  12298  cncongr2  12299  cncongrcoprm  12301  prmind2  12315  dvdsnprmd  12320  exprmfct  12333  isprm6  12342  pw2dvdslemn  12360  oddpwdclemdc  12368  sqrt2irraplemnn  12374  divnumden  12391  divdenle  12392  nn0sqrtelqelz  12401  phivalfi  12407  crth  12419  eulerth  12428  prmdivdiv  12432  reumodprminv  12449  nnnn0modprm0  12451  nnoddn2prmb  12458  pcval  12492  pcidlem  12519  pcid  12520  pcneg  12521  pc2dvds  12526  pcz  12528  pcprod  12542  prmpwdvds  12551  4sqexercise1  12594  2expltfac  12635  xpct  12640  znnen  12642  ennnfonelemg  12647  ennnfone  12669  ctinfom  12672  ctinf  12674  ssomct  12689  isstruct2im  12715  isstruct2r  12716  setsvalg  12735  setsslnid  12757  ressvalsets  12769  ressex  12770  2strbasg  12824  2stropg  12825  2strbas1g  12827  ressmulrg  12849  ressscag  12887  ressvscag  12888  ressipg  12889  restval  12949  restid2  12952  prdsex  12973  pwsval  12995  qusex  13029  fnpr2o  13043  xpsfval  13052  xpsval  13056  intopsn  13071  mgmidmo  13076  lidrididd  13086  ismnddef  13122  mndinvmod  13149  imasmnd2  13156  ismhm  13165  mhmex  13166  insubm  13189  dfgrp2  13231  grpsubval  13250  grpinvinv  13271  grpsubrcan  13285  grpsubadd  13292  grpaddsubass  13294  grpsubsub4  13297  grppnpcan2  13298  grpnpncan  13299  grpnpncan0  13300  grpnnncan2  13301  dfgrp3m  13303  dfgrp3me  13304  imasgrp2  13318  mhmmnd  13324  mulgfvalg  13329  mulgval  13330  mulgfng  13332  mulg1  13337  mulgnnp1  13338  mulgnndir  13359  mulgass  13367  mulgmodid  13369  issubg2m  13397  grpissubg  13402  isnsg  13410  isnsg3  13415  0nsg  13422  eqgfval  13430  eqger  13432  eqgen  13435  eqgcpbl  13436  quseccl  13441  isghm  13451  kerf1ghm  13482  conjghm  13484  conjsubg  13485  abladdsub  13523  ablpncan3  13525  ablsubsub23  13533  invghm  13537  subgabl  13540  mgpress  13565  rngdi  13574  rnglz  13579  imasrng  13590  srgmulgass  13623  srgrmhm  13628  isring  13634  ringo2times  13662  ringrng  13670  ringlz  13677  imasring  13698  opprrng  13711  opprrngbg  13712  opprring  13713  mulgass3  13719  dvdsrd  13728  dvdsrneg  13737  unitnegcl  13764  dvrvald  13768  dvrid  13771  dvr1  13772  dvrass  13773  dvrdir  13777  ringinvdv  13779  rhmex  13791  isrim0  13795  rhmval  13807  rhmdvdsr  13809  rhmopp  13810  elrhmunit  13811  rhmunitinv  13812  isnzr2  13818  ringelnzr  13821  issubrng2  13844  issubrg2  13875  aprap  13920  lmodvs1  13950  lmod0vs  13955  lmodvs0  13956  lmodvsmmulgdi  13957  lmodfopne  13960  lmodvneg1  13964  lss1  13996  islss3  14013  lsslss  14015  lss1d  14017  lspf  14023  lspsn  14050  lspsnneg  14054  sraval  14071  sraring  14083  qus1  14160  qusrhm  14162  cnfldui  14223  dvdsrzring  14237  mulgghm2  14242  mulgrhm  14243  znval  14270  znf1o  14285  psrbagfi  14307  psrplusgg  14312  mplgrpfi  14340  eltg2b  14398  difopn  14452  ntrcls0  14475  neii1  14491  restbasg  14512  resttopon  14515  restuni2  14521  cnrest2r  14581  tx1cn  14613  txcnp  14615  txcn  14619  txswaphmeo  14665  psmettri  14674  xmeteq0  14703  xmettri  14716  metrtri  14721  ssblex  14775  xmeter  14780  isxms2  14796  cnbl0  14878  cnblcld  14879  reopnap  14890  tgioo  14898  addcncntoplem  14905  expcn  14913  rescncf  14925  cncfcdm  14926  mulc1cncf  14933  cncfcncntop  14937  addccncf  14944  cdivcncfap  14948  negcncf  14949  cnopnap  14955  suplociccex  14969  hoverlt1  14993  hovergt0  14994  dich0  14996  limccl  15003  ellimc3apf  15004  cnplimcim  15011  limccnp2lem  15020  reldvg  15023  dvbsssg  15030  dvcjbr  15052  dvcj  15053  dvfre  15054  dvrecap  15057  dvef  15071  plyaddcl  15098  plymulcl  15099  plysubcl  15100  plyrecj  15107  reeff1olem  15115  pilem3  15127  ptolemy  15168  rplogcl  15223  rpcxpef  15238  cxprec  15254  rpcxproot  15258  rplogb1  15292  logbgt0b  15310  logbgcd1irr  15311  binom4  15323  wilthlem1  15324  sgmnncl  15332  dvdsppwf1o  15333  mersenne  15341  lgslem4  15352  lgsval  15353  lgsval2lem  15359  lgsval4a  15371  lgsdir2lem3  15379  lgsdir2  15382  lgsne0  15387  lgsprme0  15391  lgsmulsqcoprm  15395  gausslemma2dlem0a  15398  gausslemma2dlem1a  15407  2lgslem1b  15438  2lgslem2  15441  2lgsoddprm  15462  bj-nnan  15490  bj-indind  15686  bj-omtrans  15710  bj-inf2vnlem1  15724  sscoll2  15742  2omap  15750  pwtrufal  15752  sssneq  15757  pw1nct  15758  nninfsellemsuc  15767  nninfomnilem  15773  nnnninfex  15777  exmidsbthrlem  15779  qdencn  15784  trilpo  15800  trirec0  15801  apdiff  15805  iswomninnlem  15806  iswomni0  15808  redcwlpo  15812  redc0  15814  reap0  15815  cndcap  15816  dceqnconst  15817  dcapnconst  15818  neapmkv  15825  neap0mkv  15826