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  2139  mooran1  2155  eupickbi  2165  2exeu  2175  dimatis  2200  rexim  2638  r19.26  2671  r19.40  2699  rspcime  2931  rr19.28v  2960  elrab3t  2975  eueq3dc  2994  mosubt  2997  reu6  3009  sbc2iegf  3116  sbcralt  3122  sbcrext  3123  rmob  3139  csbiebt  3181  ssab2  3326  difdif  3348  uneqin  3476  indifdir  3481  undif3ss  3486  rexm  3613  eqifdc  3663  ifandc  3667  ifnebibdc  3672  difsn  3836  opprc1  3910  unissel  3948  ssmin  3973  abssexg  4300  undifexmid  4311  pwntru  4317  exmidundif  4324  exmidundifim  4325  opelopabsb  4383  elopabran  4407  sess1  4463  ordelord  4507  onin  4512  suctr  4547  abnexg  4572  ifexg  4611  ordtriexmidlem  4646  ordtri2or2exmid  4698  ontri2orexmidim  4699  tfi  4709  peano1  4721  peano2  4722  nnpredcl  4750  0nelxp  4782  0nelelxp  4783  brab2a  4808  mosubopt  4820  posng  4827  opabssxp  4829  ideqg  4911  relssres  5081  trin2  5159  dminss  5182  iota4an  5338  iota2  5347  iotam  5349  fununfun  5404  fun11uni  5431  imadiflem  5440  funimaexg  5445  fneq12  5454  fvelrnb  5729  dffo4  5830  ffnfv  5840  ffvresb  5845  fmptco  5848  fcoconst  5853  funopsn  5865  fndmexb  5912  fcof1  5962  isotr  5995  isopolem  6001  f1oiso  6005  acexmidlemcase  6053  ovprc1  6095  fnoprabg  6162  elovmporab  6262  elovmporab1w  6263  uchoice  6344  op1steq  6386  dmmpog  6418  1stconst  6430  f1o2ndf1  6437  suppfnss  6470  suppssfvg  6476  brtpos2  6495  tpostpos  6508  tposf12  6513  smores  6536  tfrlemi1  6576  tfr1onlembfn  6588  tfri1dALT  6595  tfrcllembfn  6601  freceq1  6636  freceq2  6637  frectfr  6644  omv2  6711  omsuc  6718  nnsucelsuc  6737  nntri3  6743  nnaordi  6754  nnmordi  6762  nnm00  6776  ecexr  6785  ertr  6795  swoer  6808  erth  6826  ecelqsdm  6852  iinerm  6854  ecinxp  6857  erovlem  6874  pmresg  6923  resixp  6981  elixpsn  6983  mapsnf1o  6985  dom3  7028  modom  7074  mapdom1g  7113  ssenen  7118  phpelm  7134  finexdc  7173  exmidpweq  7182  nnwetri  7189  fiintim  7204  infidc  7214  suppeqfsuppbi  7261  ssfii  7274  fiss  7277  dcfi  7281  2omap  7282  supubti  7303  supisoex  7313  ordiso2  7339  inl11  7369  omp1eomlem  7398  nnnninf  7430  nninfisol  7437  ctssexmid  7454  ismkvnex  7459  omniwomnimkv  7471  nninfwlpor  7478  nninfwlpoim  7483  nninfinfwlpo  7484  en2eleq  7511  en2other2  7512  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  acnrcl  7521  exmidaclem  7528  djuen  7531  djudoml  7539  netap  7584  2omotaplemst  7588  exmidapne  7590  cc1  7595  acnccim  7602  dmaddpqlem  7708  distrnqg  7718  ltanqi  7733  ltmnqi  7734  ltaddnq  7738  ltrnqg  7751  ltnnnq  7754  enq0sym  7763  addnq0mo  7778  mulnq0mo  7779  addnnnq0  7780  distrnq0  7790  prarloclemn  7830  prarloc  7834  ltdfpr  7837  genplt2i  7841  addnqprl  7860  addnqpru  7861  nqprl  7882  appdivnq  7894  1idprl  7921  1idpru  7922  ltexpri  7944  recexpr  7969  cauappcvgprlemdisj  7982  archrecpr  7995  addsrmo  8074  mulsrmo  8075  addsrpr  8076  mulsrpr  8077  0idsr  8098  1idsr  8099  archsr  8113  prsradd  8117  prsrlt  8118  caucvgsr  8133  map2psrprg  8136  elrealeu  8160  muladd11r  8445  negeu  8480  pncan  8495  pncan3  8497  negsub  8537  addid0  8662  addeq0  8666  posdif  8746  ltnegcon1  8754  subge0  8766  suble0  8767  lesub0  8770  reapval  8867  reapneg  8888  ap0gt0  8931  aprcl  8937  lt0ap0  8939  recextlem1  8942  recapb  8962  div0ap  8993  recrecap  9000  rec11ap  9001  recgt0  9141  mulgt1  9154  lerec2  9180  recp1lt1  9190  recreclt  9191  ledivp1  9194  negiso  9246  nnsub  9293  avglt1  9494  nnrecl  9511  nnnn0addcl  9543  elnn0nn  9555  fcdmnn0fsuppg  9568  nn0ge2m1nn  9577  zaddcl  9634  eluzmn  9878  eluzadd  9901  infregelbex  9948  divfnzn  9971  qaddcl  9985  qreccl  9992  cnref1o  10001  ge0p1rp  10036  divlt1lt  10075  divle1le  10076  addlelt  10119  xrre3  10174  xltnegi  10187  xaddval  10197  xaddcom  10213  xnegdi  10220  xposdif  10234  ixxssixx  10254  iccshftr  10346  iccshftl  10348  iccdil  10350  icccntr  10352  zltaddlt1le  10360  elfz2  10368  peano2fzr  10391  fzdcel  10394  fzsplit2  10404  fzaddel  10414  fzrev2  10441  fzrev2i  10442  fzrev3  10443  elfz1b  10446  fseq1p1m1  10450  uzsubfz0  10485  fzosubel3  10563  eluzgtdifelfzo  10564  fzofzp1b  10595  elfzomelpfzo  10598  exfzdc  10608  fvinim0ffz  10609  zsupcllemex  10612  infssuzcldc  10617  exbtwnzlemshrink  10632  qbtwnz  10635  qbtwnxr  10641  ico0  10645  elicore  10650  xqltnle  10651  apbtwnz  10658  flqge  10666  flqlt  10667  flqltnz  10671  flqbi2  10675  flqaddz  10681  flqmulnn0  10683  intfracq  10706  flqdiv  10707  q0mod  10741  q1mod  10742  mulp1mod1  10751  q2txmodxeq0  10770  modfzo0difsn  10781  frec2uzuzd  10788  frec2uzltd  10789  frec2uzrand  10791  uzennn  10822  seqfveq2g  10863  seq3split  10874  seqsplitg  10875  seq3caopr  10881  seqcaoprg  10882  seqf1oglem2  10906  seqf1og  10907  exp3vallem  10926  exp3val  10927  expnnval  10928  exp1  10931  expcl2lemap  10937  rpexpcl  10944  expnegzap  10959  mulexp  10964  mulexpzap  10965  leexp2r  10979  leexp1a  10980  sq11  10998  subsq  11032  binom2  11037  binom3  11043  zesq  11045  bernneq  11047  sq11ap  11094  zzlesq  11095  mulsubdivbinom2ap  11098  apexp1  11105  facwordi  11127  facubnd  11132  facavg  11133  bcval  11136  bcval5  11150  hashennn  11168  fihashf1rn  11176  fseq1hash  11190  hashdifsn  11209  hashdifpr  11210  hashxp  11216  hashmap  11217  fiubz  11221  fiubnn  11222  fnfz0hash  11224  ffzo0hash  11226  ssenneg  11229  hashfibclem  11231  hash2en  11240  wrdval  11252  ffz0iswrdnn0  11276  wrdsymb0  11282  ccatsymb  11315  ccatval21sw  11318  lswccatn0lsw  11324  ccatalpha  11326  ccatrcl1  11327  s111  11344  ccat1st1st  11354  lswccats1fst  11357  swrdlen2  11379  swrdfv2  11380  swrdsbslen  11383  swrds1  11385  ccatswrd  11387  pfxval  11391  pfxclg  11395  pfxmpt  11397  pfxid  11403  pfxfv0  11409  pfxtrcfv0  11411  pfxfvlsw  11412  pfxeq  11413  ccatpfx  11418  swrdpfx  11424  lenrevpfxcctswrd  11429  wrdeqs1cat  11437  cats1un  11438  swrdccatin1  11442  pfxccatin12lem2a  11444  pfxccatin12lem1  11445  pfxccatin12lem3  11449  pfxccatin12  11450  swrdccat  11452  pfxccat3a  11455  swrdccat3blem  11456  swrdccat3b  11457  reuccatpfxs1lem  11463  reuccatpfxs1  11464  s2cl  11502  s2fv0g  11504  shftfvalg  11528  ovshftex  11529  shftdm  11532  shftfib  11533  shftval  11535  shftf  11540  crre  11567  cjexp  11603  cjreim2  11614  uzin2  11697  rexuz3  11700  resqrexlemgt0  11730  resqrex  11736  sqrtgt0  11744  sqrtsq  11754  sqrtmsq  11755  absrpclap  11771  absext  11773  absmul  11779  absid  11781  absexp  11789  nn0abscl  11795  abslt  11798  absle  11799  recvalap  11807  abstri  11814  caubnd2  11827  qdenre  11912  maxabsle  11914  maxabslemval  11918  maxcl  11920  rexanre  11930  min1inf  11942  minabs  11946  minclpr  11947  mul0inf  11951  mingeb  11952  xrmaxiflemcl  11955  xrnegiso  11972  climconst2  12001  climmpt  12010  climres  12013  climcaucn  12061  sumeq1  12065  summodclem2a  12092  isumz  12100  fisumss  12103  fsumzcl2  12116  sumsnf  12120  isumclim3  12134  fsum2dlemstep  12145  fisumcom2  12149  fsumconst  12165  cvgcmpub  12187  binom  12195  binom1p  12196  binom1dif  12198  bcxmas  12200  divcnv  12208  geo2lim  12227  geoisum  12228  geoisumr  12229  geoisum1  12230  mertenslemi1  12246  mertensabs  12248  prod1dc  12297  fprodconst  12331  fprodcom2fi  12337  efcllem  12370  efcj  12384  efadd  12386  efexp  12393  efgt1p2  12406  tanvalap  12419  tanval2ap  12424  tanval3ap  12425  sinadd  12447  cosadd  12448  dvdsdc  12509  iddvdsexp  12526  dvdsadd  12547  dvds1  12564  odd2np1  12584  oddm1even  12586  m1exp1  12612  divalglemnn  12629  fldivndvdslt  12648  flodddiv4lt  12649  bitsp1  12662  bitsmod  12667  bitsfi  12668  bitscmp  12669  bitsinv1lem  12672  dvdsbnd  12677  gcdnncl  12688  zeqzmulgcd  12691  gcdneg  12703  modgcd  12712  bezoutlemex  12722  bezoutlemeu  12728  dfgcd3  12731  gcdzeq  12743  dvdssq  12752  algrf  12767  eucalgval2  12775  eucalgcvga  12780  lcmval  12785  gcddvdslcm  12795  lcmneg  12796  coprmgcdb  12810  qredeu  12819  divgcdcoprm0  12823  divgcdcoprmex  12824  cncongr1  12825  cncongr2  12826  cncongrcoprm  12828  prmind2  12842  dvdsnprmd  12847  exprmfct  12860  isprm6  12869  pw2dvdslemn  12887  oddpwdclemdc  12895  sqrt2irraplemnn  12901  divnumden  12918  divdenle  12919  nn0sqrtelqelz  12928  phivalfi  12934  crth  12946  eulerth  12955  prmdivdiv  12959  reumodprminv  12976  nnnn0modprm0  12978  nnoddn2prmb  12985  pcval  13019  pcidlem  13046  pcid  13047  pcneg  13048  pc2dvds  13053  pcz  13055  pcprod  13069  prmpwdvds  13078  4sqexercise1  13121  2expltfac  13162  ballotfilemfval  13173  ballotfilemefi  13181  ballotfilemodife  13184  ballotfilem4  13185  ballotfilemsval  13196  ballotfilemieq  13204  ballotfilemrv  13207  ballotfilemrinv0  13220  xpct  13231  znnen  13233  ennnfonelemg  13238  ennnfone  13260  ctinfom  13263  ctinf  13265  ssomct  13280  isstruct2im  13306  isstruct2r  13307  setsvalg  13326  setsslnid  13348  ressvalsets  13361  ressex  13362  2strbasg  13417  2stropg  13418  2strbas1g  13420  ressmulrg  13442  ressscag  13480  ressvscag  13481  ressipg  13482  restval  13542  restid2  13545  prdsex  13566  pwsval  13588  qusex  13622  fnpr2o  13636  xpsfval  13645  xpsval  13649  intopsn  13664  mgmidmo  13669  lidrididd  13679  ismnddef  13715  mndinvmod  13742  imasmnd2  13749  ismhm  13758  mhmex  13759  insubm  13782  dfgrp2  13824  grpsubval  13843  grpinvinv  13864  grpsubrcan  13878  grpsubadd  13885  grpaddsubass  13887  grpsubsub4  13890  grppnpcan2  13891  grpnpncan  13892  grpnpncan0  13893  grpnnncan2  13894  dfgrp3m  13896  dfgrp3me  13897  imasgrp2  13911  mhmmnd  13917  mulgfvalg  13922  mulgval  13923  mulgfng  13925  mulg1  13930  mulgnnp1  13931  mulgnndir  13952  mulgass  13960  mulgmodid  13962  issubg2m  13990  grpissubg  13995  isnsg  14003  isnsg3  14008  0nsg  14015  eqgfval  14023  eqger  14025  eqgen  14028  eqgcpbl  14029  quseccl  14034  isghm  14044  kerf1ghm  14075  conjghm  14077  conjsubg  14078  abladdsub  14116  ablpncan3  14118  ablsubsub23  14126  invghm  14130  subgabl  14133  mgpress  14159  rngdi  14168  rnglz  14173  imasrng  14184  srgmulgass  14217  srgrmhm  14222  isring  14228  ringo2times  14256  ringrng  14264  ringlz  14271  imasring  14292  opprrng  14305  opprrngbg  14306  opprring  14307  mulgass3  14314  dvdsrd  14324  dvdsrneg  14333  unitnegcl  14360  dvrvald  14364  dvrid  14367  dvr1  14368  dvrass  14369  dvrdir  14373  ringinvdv  14375  rhmex  14387  isrim0  14391  rhmval  14403  rhmdvdsr  14405  rhmopp  14406  elrhmunit  14407  rhmunitinv  14408  isnzr2  14414  ringelnzr  14417  issubrng2  14441  issubrg2  14472  ringunitap  14516  aprap  14521  aprnzr  14522  opprdrng  14543  lmodvs1  14576  lmod0vs  14581  lmodvs0  14582  lmodvsmmulgdi  14583  lmodfopne  14586  lmodvneg1  14590  lss1  14622  islss3  14639  lsslss  14641  lss1d  14643  lspf  14649  lspsn  14676  lspsnneg  14680  sraval  14697  sraring  14709  qus1  14786  qusrhm  14788  cnfldui  14849  dvdsrzring  14863  mulgghm2  14868  mulgrhm  14869  znval  14896  znf1o  14911  psrbagfi  14935  psrbagconcl  14939  psrplusgg  14945  mplgrpfi  14973  eltg2b  15031  difopn  15085  ntrcls0  15108  neii1  15124  restbasg  15145  resttopon  15148  restuni2  15154  cnrest2r  15214  tx1cn  15246  txcnp  15248  txcn  15252  txswaphmeo  15298  psmettri  15307  xmeteq0  15336  xmettri  15349  metrtri  15354  ssblex  15408  xmeter  15413  isxms2  15429  cnbl0  15511  cnblcld  15512  reopnap  15523  tgioo  15531  addcncntoplem  15538  expcn  15546  rescncf  15558  cncfcdm  15559  mulc1cncf  15566  cncfcncntop  15570  addccncf  15577  cdivcncfap  15581  negcncf  15582  cnopnap  15588  suplociccex  15602  hoverlt1  15626  hovergt0  15627  dich0  15629  limccl  15636  ellimc3apf  15637  cnplimcim  15644  limccnp2lem  15653  reldvg  15656  dvbsssg  15663  dvcjbr  15685  dvcj  15686  dvfre  15687  dvrecap  15690  dvef  15704  plyaddcl  15731  plymulcl  15732  plysubcl  15733  plyrecj  15740  reeff1olem  15748  pilem3  15760  ptolemy  15801  rplogcl  15856  rpcxpef  15871  cxprec  15887  rpcxproot  15891  rplogb1  15925  logbgt0b  15943  logbgcd1irr  15944  binom4  15956  wilthlem1  15960  sgmnncl  15968  dvdsppwf1o  15969  mersenne  15977  lgslem4  15988  lgsval  15989  lgsval2lem  15995  lgsval4a  16007  lgsdir2lem3  16015  lgsdir2  16018  lgsne0  16023  lgsprme0  16027  lgsmulsqcoprm  16031  gausslemma2dlem0a  16034  gausslemma2dlem1a  16043  2lgslem1b  16074  2lgslem2  16077  2lgsoddprm  16098  struct2slots2dom  16145  structvtxval  16146  structiedg0val  16147  struct2griedg  16153  edgstruct  16171  uhgr0vb  16191  incistruhgr  16197  umgrvad2edg  16318  uspgredg2vlem  16327  uspgredg2v  16328  usgredg2v  16331  ushgredgedg  16333  ushgredgedgloop  16335  usgr0vb  16340  uhgr0vusgr  16345  edg0usgr  16354  subupgr  16380  upgrspanop  16390  umgrspanop  16391  usgrspanop  16392  vtxdgfval  16395  wksfval  16429  wlkpropg  16431  uspgr2wlkeq2  16473  uspgr2wlkeqi  16474  upgr2wlkdc  16484  trlsex  16494  clwwlkccatlem  16507  clwwlkng  16512  clwwlkext2edg  16529  clwwlknccat  16530  umgr2cwwkdifex  16532  clwwlknonel  16539  clwwlknonccat  16540  clwwlknonex2lem2  16545  clwwlknun  16548  eupthsg  16552  eupth2lem3lem6fi  16578  bj-nnan  16620  bj-indind  16814  bj-omtrans  16838  bj-inf2vnlem1  16852  sscoll2  16870  pw1map  16881  pwtrufal  16883  sssneq  16888  pw1nct  16889  exmidnotnotr  16891  nninfsellemsuc  16902  nninfomnilem  16908  nnnninfex  16912  exmidsbthrlem  16914  qdencn  16919  trilpo  16939  trirec0  16940  apdiff  16944  iswomninnlem  16946  iswomni0  16948  redcwlpo  16952  redc0  16954  reap0  16955  cndcap  16956  dceqnconst  16958  dcapnconst  16959  neapmkv  16966  neap0mkv  16967