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  535  simplrl  537  simprll  539  simprrl  541  anabs1  574  jcab  607  pm4.38  609  pm5.21  703  ioran  760  pm3.14  761  pm4.44  787  ordi  824  pm4.39  830  animorl  831  animorlr  833  pm5.16  836  pm5.54dc  926  intnanr  938  intnanrd  940  dcan  942  dedlema  978  dedlemb  979  pm4.42r  980  prlem2  983  ifpdc  988  dfifp2dc  990  simp1l  1048  simp2l  1050  simp3l  1052  3anandis  1384  xordc1  1438  anxordi  1445  falantru  1448  19.26  1530  exsimpl  1666  sbequ2  1818  sbcof2  1859  sbequilem  1887  sbequ8  1896  euan  2137  mooran1  2153  eupickbi  2163  2exeu  2173  dimatis  2198  rexim  2636  r19.26  2669  r19.40  2697  rspcime  2927  rr19.28v  2956  elrab3t  2971  eueq3dc  2990  mosubt  2993  reu6  3005  sbc2iegf  3112  sbcralt  3118  sbcrext  3119  rmob  3135  csbiebt  3177  ssab2  3321  difdif  3343  uneqin  3471  indifdir  3476  undif3ss  3481  rexm  3608  eqifdc  3658  ifandc  3662  ifnebibdc  3667  difsn  3830  opprc1  3904  unissel  3942  ssmin  3967  abssexg  4294  undifexmid  4305  pwntru  4311  exmidundif  4318  exmidundifim  4319  opelopabsb  4377  elopabran  4401  sess1  4457  ordelord  4501  onin  4506  suctr  4541  abnexg  4566  ifexg  4605  ordtriexmidlem  4640  ordtri2or2exmid  4692  ontri2orexmidim  4693  tfi  4703  peano1  4715  peano2  4716  nnpredcl  4744  0nelxp  4776  0nelelxp  4777  brab2a  4802  mosubopt  4814  posng  4821  opabssxp  4823  ideqg  4905  relssres  5075  trin2  5153  dminss  5176  iota4an  5332  iota2  5341  iotam  5343  fununfun  5398  fun11uni  5425  imadiflem  5434  funimaexg  5439  fneq12  5448  fvelrnb  5723  dffo4  5824  ffnfv  5834  ffvresb  5839  fmptco  5842  fcoconst  5847  funopsn  5859  fndmexb  5906  fcof1  5955  isotr  5988  isopolem  5994  f1oiso  5998  acexmidlemcase  6044  ovprc1  6086  fnoprabg  6153  elovmporab  6253  elovmporab1w  6254  uchoice  6330  op1steq  6372  dmmpog  6404  1stconst  6416  f1o2ndf1  6423  suppfnss  6456  suppssfvg  6462  brtpos2  6481  tpostpos  6494  tposf12  6499  smores  6522  tfrlemi1  6562  tfr1onlembfn  6574  tfri1dALT  6581  tfrcllembfn  6587  freceq1  6622  freceq2  6623  frectfr  6630  omv2  6697  omsuc  6704  nnsucelsuc  6723  nntri3  6729  nnaordi  6740  nnmordi  6748  nnm00  6762  ecexr  6771  ertr  6781  swoer  6794  erth  6812  ecelqsdm  6838  iinerm  6840  ecinxp  6843  erovlem  6860  pmresg  6909  resixp  6967  elixpsn  6969  mapsnf1o  6971  dom3  7014  modom  7060  mapdom1g  7099  ssenen  7104  phpelm  7120  finexdc  7159  exmidpweq  7168  nnwetri  7175  fiintim  7190  infidc  7200  suppeqfsuppbi  7247  ssfii  7260  fiss  7263  dcfi  7267  2omap  7268  supubti  7289  supisoex  7299  ordiso2  7325  inl11  7355  omp1eomlem  7384  nnnninf  7416  nninfisol  7423  ctssexmid  7440  ismkvnex  7445  omniwomnimkv  7457  nninfwlpor  7464  nninfwlpoim  7469  nninfinfwlpo  7470  en2eleq  7497  en2other2  7498  exmidfodomrlemr  7504  exmidfodomrlemrALT  7505  acnrcl  7507  exmidaclem  7514  djuen  7517  djudoml  7525  netap  7567  2omotaplemst  7571  exmidapne  7573  cc1  7578  acnccim  7585  dmaddpqlem  7691  distrnqg  7701  ltanqi  7716  ltmnqi  7717  ltaddnq  7721  ltrnqg  7734  ltnnnq  7737  enq0sym  7746  addnq0mo  7761  mulnq0mo  7762  addnnnq0  7763  distrnq0  7773  prarloclemn  7813  prarloc  7817  ltdfpr  7820  genplt2i  7824  addnqprl  7843  addnqpru  7844  nqprl  7865  appdivnq  7877  1idprl  7904  1idpru  7905  ltexpri  7927  recexpr  7952  cauappcvgprlemdisj  7965  archrecpr  7978  addsrmo  8057  mulsrmo  8058  addsrpr  8059  mulsrpr  8060  0idsr  8081  1idsr  8082  archsr  8096  prsradd  8100  prsrlt  8101  caucvgsr  8116  map2psrprg  8119  elrealeu  8143  muladd11r  8428  negeu  8463  pncan  8478  pncan3  8480  negsub  8520  addid0  8645  posdif  8728  ltnegcon1  8736  subge0  8748  suble0  8749  lesub0  8752  reapval  8849  reapneg  8870  ap0gt0  8913  aprcl  8919  lt0ap0  8921  recextlem1  8924  recapb  8944  div0ap  8975  recrecap  8982  rec11ap  8983  recgt0  9123  mulgt1  9136  lerec2  9162  recp1lt1  9172  recreclt  9173  ledivp1  9176  negiso  9228  nnsub  9275  avglt1  9476  nnrecl  9493  nnnn0addcl  9525  elnn0nn  9537  fcdmnn0fsuppg  9550  nn0ge2m1nn  9559  zaddcl  9616  eluzmn  9859  eluzadd  9882  infregelbex  9929  divfnzn  9952  qaddcl  9966  qreccl  9973  cnref1o  9982  ge0p1rp  10017  divlt1lt  10056  divle1le  10057  addlelt  10100  xrre3  10154  xltnegi  10167  xaddval  10177  xaddcom  10193  xnegdi  10200  xposdif  10214  ixxssixx  10234  iccshftr  10326  iccshftl  10328  iccdil  10330  icccntr  10332  zltaddlt1le  10340  elfz2  10348  peano2fzr  10370  fzdcel  10373  fzsplit2  10383  fzaddel  10392  fzrev2  10418  fzrev2i  10419  fzrev3  10420  elfz1b  10423  fseq1p1m1  10427  uzsubfz0  10462  fzosubel3  10540  eluzgtdifelfzo  10541  fzofzp1b  10572  elfzomelpfzo  10575  exfzdc  10585  fvinim0ffz  10586  zsupcllemex  10589  infssuzcldc  10594  exbtwnzlemshrink  10607  qbtwnz  10610  qbtwnxr  10616  ico0  10620  elicore  10625  xqltnle  10626  apbtwnz  10633  flqge  10641  flqlt  10642  flqltnz  10646  flqbi2  10650  flqaddz  10656  flqmulnn0  10658  intfracq  10681  flqdiv  10682  q0mod  10716  q1mod  10717  mulp1mod1  10726  q2txmodxeq0  10745  modfzo0difsn  10756  frec2uzuzd  10763  frec2uzltd  10764  frec2uzrand  10766  uzennn  10797  seqfveq2g  10838  seq3split  10849  seqsplitg  10850  seq3caopr  10856  seqcaoprg  10857  seqf1oglem2  10881  seqf1og  10882  exp3vallem  10901  exp3val  10902  expnnval  10903  exp1  10906  expcl2lemap  10912  rpexpcl  10919  expnegzap  10934  mulexp  10939  mulexpzap  10940  leexp2r  10954  leexp1a  10955  sq11  10973  subsq  11007  binom2  11012  binom3  11018  zesq  11019  bernneq  11021  sq11ap  11068  zzlesq  11069  mulsubdivbinom2ap  11072  apexp1  11079  facwordi  11101  facubnd  11106  facavg  11107  bcval  11110  bcval5  11124  hashennn  11141  fihashf1rn  11149  fseq1hash  11163  hashdifsn  11182  hashdifpr  11183  hashxp  11189  fiubz  11192  fiubnn  11193  fnfz0hash  11195  ffzo0hash  11197  ssenneg  11200  hashfibclem  11202  hash2en  11211  wrdval  11223  ffz0iswrdnn0  11247  wrdsymb0  11253  ccatsymb  11286  ccatval21sw  11289  lswccatn0lsw  11295  ccatalpha  11297  ccatrcl1  11298  s111  11315  ccat1st1st  11325  lswccats1fst  11328  swrdlen2  11350  swrdfv2  11351  swrdsbslen  11354  swrds1  11356  ccatswrd  11358  pfxval  11362  pfxclg  11366  pfxmpt  11368  pfxid  11374  pfxfv0  11380  pfxtrcfv0  11382  pfxfvlsw  11383  pfxeq  11384  ccatpfx  11389  swrdpfx  11395  lenrevpfxcctswrd  11400  wrdeqs1cat  11408  cats1un  11409  swrdccatin1  11413  pfxccatin12lem2a  11415  pfxccatin12lem1  11416  pfxccatin12lem3  11420  pfxccatin12  11421  swrdccat  11423  pfxccat3a  11426  swrdccat3blem  11427  swrdccat3b  11428  reuccatpfxs1lem  11434  reuccatpfxs1  11435  s2cl  11473  s2fv0g  11475  shftfvalg  11499  ovshftex  11500  shftdm  11503  shftfib  11504  shftval  11506  shftf  11511  crre  11538  cjexp  11574  cjreim2  11585  uzin2  11668  rexuz3  11671  resqrexlemgt0  11701  resqrex  11707  sqrtgt0  11715  sqrtsq  11725  sqrtmsq  11726  absrpclap  11742  absext  11744  absmul  11750  absid  11752  absexp  11760  nn0abscl  11766  abslt  11769  absle  11770  recvalap  11778  abstri  11785  caubnd2  11798  qdenre  11883  maxabsle  11885  maxabslemval  11889  maxcl  11891  rexanre  11901  min1inf  11913  minabs  11917  minclpr  11918  mul0inf  11922  mingeb  11923  xrmaxiflemcl  11926  xrnegiso  11943  climconst2  11972  climmpt  11981  climres  11984  climcaucn  12032  sumeq1  12036  summodclem2a  12063  isumz  12071  fisumss  12074  fsumzcl2  12087  sumsnf  12091  isumclim3  12105  fsum2dlemstep  12116  fisumcom2  12120  fsumconst  12136  cvgcmpub  12158  binom  12166  binom1p  12167  binom1dif  12169  bcxmas  12171  divcnv  12179  geo2lim  12198  geoisum  12199  geoisumr  12200  geoisum1  12201  mertenslemi1  12217  mertensabs  12219  prod1dc  12268  fprodconst  12302  fprodcom2fi  12308  efcllem  12341  efcj  12355  efadd  12357  efexp  12364  efgt1p2  12377  tanvalap  12390  tanval2ap  12395  tanval3ap  12396  sinadd  12418  cosadd  12419  dvdsdc  12480  iddvdsexp  12497  dvdsadd  12518  dvds1  12535  odd2np1  12555  oddm1even  12557  m1exp1  12583  divalglemnn  12600  fldivndvdslt  12619  flodddiv4lt  12620  bitsp1  12633  bitsmod  12638  bitsfi  12639  bitscmp  12640  bitsinv1lem  12643  dvdsbnd  12648  gcdnncl  12659  zeqzmulgcd  12662  gcdneg  12674  modgcd  12683  bezoutlemex  12693  bezoutlemeu  12699  dfgcd3  12702  gcdzeq  12714  dvdssq  12723  algrf  12738  eucalgval2  12746  eucalgcvga  12751  lcmval  12756  gcddvdslcm  12766  lcmneg  12767  coprmgcdb  12781  qredeu  12790  divgcdcoprm0  12794  divgcdcoprmex  12795  cncongr1  12796  cncongr2  12797  cncongrcoprm  12799  prmind2  12813  dvdsnprmd  12818  exprmfct  12831  isprm6  12840  pw2dvdslemn  12858  oddpwdclemdc  12866  sqrt2irraplemnn  12872  divnumden  12889  divdenle  12890  nn0sqrtelqelz  12899  phivalfi  12905  crth  12917  eulerth  12926  prmdivdiv  12930  reumodprminv  12947  nnnn0modprm0  12949  nnoddn2prmb  12956  pcval  12990  pcidlem  13017  pcid  13018  pcneg  13019  pc2dvds  13024  pcz  13026  pcprod  13040  prmpwdvds  13049  4sqexercise1  13092  2expltfac  13133  xpct  13139  znnen  13141  ennnfonelemg  13146  ennnfone  13168  ctinfom  13171  ctinf  13173  ssomct  13188  isstruct2im  13214  isstruct2r  13215  setsvalg  13234  setsslnid  13256  ressvalsets  13269  ressex  13270  2strbasg  13325  2stropg  13326  2strbas1g  13328  ressmulrg  13350  ressscag  13388  ressvscag  13389  ressipg  13390  restval  13450  restid2  13453  prdsex  13474  pwsval  13496  qusex  13530  fnpr2o  13544  xpsfval  13553  xpsval  13557  intopsn  13572  mgmidmo  13577  lidrididd  13587  ismnddef  13623  mndinvmod  13650  imasmnd2  13657  ismhm  13666  mhmex  13667  insubm  13690  dfgrp2  13732  grpsubval  13751  grpinvinv  13772  grpsubrcan  13786  grpsubadd  13793  grpaddsubass  13795  grpsubsub4  13798  grppnpcan2  13799  grpnpncan  13800  grpnpncan0  13801  grpnnncan2  13802  dfgrp3m  13804  dfgrp3me  13805  imasgrp2  13819  mhmmnd  13825  mulgfvalg  13830  mulgval  13831  mulgfng  13833  mulg1  13838  mulgnnp1  13839  mulgnndir  13860  mulgass  13868  mulgmodid  13870  issubg2m  13898  grpissubg  13903  isnsg  13911  isnsg3  13916  0nsg  13923  eqgfval  13931  eqger  13933  eqgen  13936  eqgcpbl  13937  quseccl  13942  isghm  13952  kerf1ghm  13983  conjghm  13985  conjsubg  13986  abladdsub  14024  ablpncan3  14026  ablsubsub23  14034  invghm  14038  subgabl  14041  mgpress  14067  rngdi  14076  rnglz  14081  imasrng  14092  srgmulgass  14125  srgrmhm  14130  isring  14136  ringo2times  14164  ringrng  14172  ringlz  14179  imasring  14200  opprrng  14213  opprrngbg  14214  opprring  14215  mulgass3  14221  dvdsrd  14231  dvdsrneg  14240  unitnegcl  14267  dvrvald  14271  dvrid  14274  dvr1  14275  dvrass  14276  dvrdir  14280  ringinvdv  14282  rhmex  14294  isrim0  14298  rhmval  14310  rhmdvdsr  14312  rhmopp  14313  elrhmunit  14314  rhmunitinv  14315  isnzr2  14321  ringelnzr  14324  issubrng2  14347  issubrg2  14378  aprap  14424  aprnzr  14425  lmodvs1  14456  lmod0vs  14461  lmodvs0  14462  lmodvsmmulgdi  14463  lmodfopne  14466  lmodvneg1  14470  lss1  14502  islss3  14519  lsslss  14521  lss1d  14523  lspf  14529  lspsn  14556  lspsnneg  14560  sraval  14577  sraring  14589  qus1  14666  qusrhm  14668  cnfldui  14729  dvdsrzring  14743  mulgghm2  14748  mulgrhm  14749  znval  14776  znf1o  14791  psrbagfi  14815  psrbagconcl  14819  psrplusgg  14825  mplgrpfi  14853  eltg2b  14911  difopn  14965  ntrcls0  14988  neii1  15004  restbasg  15025  resttopon  15028  restuni2  15034  cnrest2r  15094  tx1cn  15126  txcnp  15128  txcn  15132  txswaphmeo  15178  psmettri  15187  xmeteq0  15216  xmettri  15229  metrtri  15234  ssblex  15288  xmeter  15293  isxms2  15309  cnbl0  15391  cnblcld  15392  reopnap  15403  tgioo  15411  addcncntoplem  15418  expcn  15426  rescncf  15438  cncfcdm  15439  mulc1cncf  15446  cncfcncntop  15450  addccncf  15457  cdivcncfap  15461  negcncf  15462  cnopnap  15468  suplociccex  15482  hoverlt1  15506  hovergt0  15507  dich0  15509  limccl  15516  ellimc3apf  15517  cnplimcim  15524  limccnp2lem  15533  reldvg  15536  dvbsssg  15543  dvcjbr  15565  dvcj  15566  dvfre  15567  dvrecap  15570  dvef  15584  plyaddcl  15611  plymulcl  15612  plysubcl  15613  plyrecj  15620  reeff1olem  15628  pilem3  15640  ptolemy  15681  rplogcl  15736  rpcxpef  15751  cxprec  15767  rpcxproot  15771  rplogb1  15805  logbgt0b  15823  logbgcd1irr  15824  binom4  15836  wilthlem1  15840  sgmnncl  15848  dvdsppwf1o  15849  mersenne  15857  lgslem4  15868  lgsval  15869  lgsval2lem  15875  lgsval4a  15887  lgsdir2lem3  15895  lgsdir2  15898  lgsne0  15903  lgsprme0  15907  lgsmulsqcoprm  15911  gausslemma2dlem0a  15914  gausslemma2dlem1a  15923  2lgslem1b  15954  2lgslem2  15957  2lgsoddprm  15978  struct2slots2dom  16025  structvtxval  16026  structiedg0val  16027  struct2griedg  16033  edgstruct  16051  uhgr0vb  16071  incistruhgr  16077  umgrvad2edg  16198  uspgredg2vlem  16207  uspgredg2v  16208  usgredg2v  16211  ushgredgedg  16213  ushgredgedgloop  16215  usgr0vb  16220  uhgr0vusgr  16225  edg0usgr  16234  subupgr  16260  upgrspanop  16270  umgrspanop  16271  usgrspanop  16272  vtxdgfval  16275  wksfval  16309  wlkpropg  16311  uspgr2wlkeq2  16353  uspgr2wlkeqi  16354  upgr2wlkdc  16364  trlsex  16374  clwwlkccatlem  16387  clwwlkng  16392  clwwlkext2edg  16409  clwwlknccat  16410  umgr2cwwkdifex  16412  clwwlknonel  16419  clwwlknonccat  16420  clwwlknonex2lem2  16425  clwwlknun  16428  eupthsg  16432  eupth2lem3lem6fi  16458  bj-nnan  16500  bj-indind  16694  bj-omtrans  16718  bj-inf2vnlem1  16732  sscoll2  16750  pw1map  16761  pwtrufal  16763  sssneq  16768  pw1nct  16769  exmidnotnotr  16771  nninfsellemsuc  16782  nninfomnilem  16788  nnnninfex  16792  exmidsbthrlem  16794  qdencn  16799  trilpo  16819  trirec0  16820  apdiff  16824  iswomninnlem  16826  iswomni0  16828  redcwlpo  16832  redc0  16834  reap0  16835  cndcap  16836  dceqnconst  16837  dcapnconst  16838  neapmkv  16845  neap0mkv  16846