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  605  pm4.38  607  pm5.21  700  ioran  757  pm3.14  758  pm4.44  784  ordi  821  pm4.39  827  animorl  828  animorlr  830  pm5.16  833  pm5.54dc  923  intnanr  935  intnanrd  937  dcan  939  dedlema  975  dedlemb  976  pm4.42r  977  prlem2  980  ifpdc  985  dfifp2dc  987  simp1l  1045  simp2l  1047  simp3l  1049  3anandis  1381  xordc1  1435  anxordi  1442  falantru  1445  19.26  1527  exsimpl  1663  sbequ2  1815  sbcof2  1856  sbequilem  1884  sbequ8  1893  euan  2134  mooran1  2150  eupickbi  2160  2exeu  2170  dimatis  2195  rexim  2624  r19.26  2657  r19.40  2685  rspcime  2914  rr19.28v  2943  elrab3t  2958  eueq3dc  2977  mosubt  2980  reu6  2992  sbc2iegf  3099  sbcralt  3105  sbcrext  3106  rmob  3122  csbiebt  3164  ssab2  3308  difdif  3329  uneqin  3455  indifdir  3460  undif3ss  3465  rexm  3591  eqifdc  3639  ifandc  3643  ifnebibdc  3648  difsn  3805  opprc1  3879  unissel  3917  ssmin  3942  abssexg  4266  undifexmid  4277  pwntru  4283  exmidundif  4290  exmidundifim  4291  opelopabsb  4348  elopabran  4372  sess1  4428  ordelord  4472  onin  4477  suctr  4512  abnexg  4537  ifexg  4576  ordtriexmidlem  4611  ordtri2or2exmid  4663  ontri2orexmidim  4664  tfi  4674  peano1  4686  peano2  4687  nnpredcl  4715  0nelxp  4747  0nelelxp  4748  brab2a  4772  mosubopt  4784  posng  4791  opabssxp  4793  ideqg  4873  relssres  5043  trin2  5120  dminss  5143  iota4an  5299  iota2  5308  iotam  5310  fununfun  5364  fun11uni  5391  imadiflem  5400  funimaexg  5405  fneq12  5414  fvelrnb  5683  dffo4  5785  ffnfv  5795  ffvresb  5800  fmptco  5803  fcoconst  5808  funopsn  5819  fcof1  5913  isotr  5946  isopolem  5952  f1oiso  5956  acexmidlemcase  6002  ovprc1  6044  fnoprabg  6111  elovmporab  6211  elovmporab1w  6212  uchoice  6289  op1steq  6331  dmmpog  6361  1stconst  6373  f1o2ndf1  6380  brtpos2  6403  tpostpos  6416  tposf12  6421  smores  6444  tfrlemi1  6484  tfr1onlembfn  6496  tfri1dALT  6503  tfrcllembfn  6509  freceq1  6544  freceq2  6545  frectfr  6552  omv2  6619  omsuc  6626  nnsucelsuc  6645  nntri3  6651  nnaordi  6662  nnmordi  6670  nnm00  6684  ecexr  6693  ertr  6703  swoer  6716  erth  6734  ecelqsdm  6760  iinerm  6762  ecinxp  6765  erovlem  6782  pmresg  6831  resixp  6888  elixpsn  6890  mapsnf1o  6892  dom3  6935  mapdom1g  7016  ssenen  7020  phpelm  7036  finexdc  7072  exmidpweq  7079  nnwetri  7086  fiintim  7101  infidc  7109  ssfii  7149  fiss  7152  dcfi  7156  supubti  7174  supisoex  7184  ordiso2  7210  inl11  7240  omp1eomlem  7269  nnnninf  7301  nninfisol  7308  ctssexmid  7325  ismkvnex  7330  omniwomnimkv  7342  nninfwlpor  7349  nninfwlpoim  7354  nninfinfwlpo  7355  en2eleq  7381  en2other2  7382  exmidfodomrlemr  7388  exmidfodomrlemrALT  7389  acnrcl  7391  exmidaclem  7398  djuen  7401  djudoml  7409  netap  7448  2omotaplemst  7452  exmidapne  7454  cc1  7459  acnccim  7466  dmaddpqlem  7572  distrnqg  7582  ltanqi  7597  ltmnqi  7598  ltaddnq  7602  ltrnqg  7615  ltnnnq  7618  enq0sym  7627  addnq0mo  7642  mulnq0mo  7643  addnnnq0  7644  distrnq0  7654  prarloclemn  7694  prarloc  7698  ltdfpr  7701  genplt2i  7705  addnqprl  7724  addnqpru  7725  nqprl  7746  appdivnq  7758  1idprl  7785  1idpru  7786  ltexpri  7808  recexpr  7833  cauappcvgprlemdisj  7846  archrecpr  7859  addsrmo  7938  mulsrmo  7939  addsrpr  7940  mulsrpr  7941  0idsr  7962  1idsr  7963  archsr  7977  prsradd  7981  prsrlt  7982  caucvgsr  7997  map2psrprg  8000  elrealeu  8024  muladd11r  8310  negeu  8345  pncan  8360  pncan3  8362  negsub  8402  addid0  8527  posdif  8610  ltnegcon1  8618  subge0  8630  suble0  8631  lesub0  8634  reapval  8731  reapneg  8752  ap0gt0  8795  aprcl  8801  lt0ap0  8803  recextlem1  8806  recapb  8826  div0ap  8857  recrecap  8864  rec11ap  8865  recgt0  9005  mulgt1  9018  lerec2  9044  recp1lt1  9054  recreclt  9055  ledivp1  9058  negiso  9110  nnsub  9157  avglt1  9358  nnrecl  9375  nnnn0addcl  9407  elnn0nn  9419  nn0ge2m1nn  9437  zaddcl  9494  eluzadd  9759  infregelbex  9801  divfnzn  9824  qaddcl  9838  qreccl  9845  cnref1o  9854  ge0p1rp  9889  divlt1lt  9928  divle1le  9929  addlelt  9972  xrre3  10026  xltnegi  10039  xaddval  10049  xaddcom  10065  xnegdi  10072  xposdif  10086  ixxssixx  10106  iccshftr  10198  iccshftl  10200  iccdil  10202  icccntr  10204  zltaddlt1le  10211  elfz2  10219  peano2fzr  10241  fzdcel  10244  fzsplit2  10254  fzaddel  10263  fzrev2  10289  fzrev2i  10290  fzrev3  10291  elfz1b  10294  fseq1p1m1  10298  uzsubfz0  10333  fzosubel3  10410  eluzgtdifelfzo  10411  fzofzp1b  10442  elfzomelpfzo  10445  exfzdc  10454  fvinim0ffz  10455  zsupcllemex  10458  infssuzcldc  10463  exbtwnzlemshrink  10476  qbtwnz  10479  qbtwnxr  10485  ico0  10489  elicore  10494  xqltnle  10495  apbtwnz  10502  flqge  10510  flqlt  10511  flqltnz  10515  flqbi2  10519  flqaddz  10525  flqmulnn0  10527  intfracq  10550  flqdiv  10551  q0mod  10585  q1mod  10586  mulp1mod1  10595  q2txmodxeq0  10614  modfzo0difsn  10625  frec2uzuzd  10632  frec2uzltd  10633  frec2uzrand  10635  uzennn  10666  seqfveq2g  10707  seq3split  10718  seqsplitg  10719  seq3caopr  10725  seqcaoprg  10726  seqf1oglem2  10750  seqf1og  10751  exp3vallem  10770  exp3val  10771  expnnval  10772  exp1  10775  expcl2lemap  10781  rpexpcl  10788  expnegzap  10803  mulexp  10808  mulexpzap  10809  leexp2r  10823  leexp1a  10824  sq11  10842  subsq  10876  binom2  10881  binom3  10887  zesq  10888  bernneq  10890  sq11ap  10937  zzlesq  10938  mulsubdivbinom2ap  10941  apexp1  10948  facwordi  10970  facubnd  10975  facavg  10976  bcval  10979  bcval5  10993  hashennn  11010  fihashf1rn  11018  fseq1hash  11031  hashdifsn  11049  hashdifpr  11050  hashxp  11056  fiubz  11059  fiubnn  11060  fnfz0hash  11062  ffzo0hash  11064  hash2en  11073  wrdval  11082  ffz0iswrdnn0  11106  wrdsymb0  11112  ccatsymb  11145  ccatval21sw  11148  lswccatn0lsw  11154  s111  11172  ccat1st1st  11180  lswccats1fst  11183  swrdlen2  11202  swrdfv2  11203  swrdsbslen  11206  swrds1  11208  ccatswrd  11210  pfxval  11214  pfxclg  11218  pfxmpt  11220  pfxid  11226  pfxfv0  11232  pfxtrcfv0  11234  pfxfvlsw  11235  pfxeq  11236  ccatpfx  11241  swrdpfx  11247  lenrevpfxcctswrd  11252  wrdeqs1cat  11260  cats1un  11261  swrdccatin1  11265  pfxccatin12lem2a  11267  pfxccatin12lem1  11268  pfxccatin12lem3  11272  pfxccatin12  11273  swrdccat  11275  pfxccat3a  11278  swrdccat3blem  11279  swrdccat3b  11280  reuccatpfxs1lem  11286  reuccatpfxs1  11287  s2cl  11325  s2fv0g  11327  shftfvalg  11337  ovshftex  11338  shftdm  11341  shftfib  11342  shftval  11344  shftf  11349  crre  11376  cjexp  11412  cjreim2  11423  uzin2  11506  rexuz3  11509  resqrexlemgt0  11539  resqrex  11545  sqrtgt0  11553  sqrtsq  11563  sqrtmsq  11564  absrpclap  11580  absext  11582  absmul  11588  absid  11590  absexp  11598  nn0abscl  11604  abslt  11607  absle  11608  recvalap  11616  abstri  11623  caubnd2  11636  qdenre  11721  maxabsle  11723  maxabslemval  11727  maxcl  11729  rexanre  11739  min1inf  11751  minabs  11755  minclpr  11756  mul0inf  11760  mingeb  11761  xrmaxiflemcl  11764  xrnegiso  11781  climconst2  11810  climmpt  11819  climres  11822  climcaucn  11870  sumeq1  11874  summodclem2a  11900  isumz  11908  fisumss  11911  fsumzcl2  11924  sumsnf  11928  isumclim3  11942  fsum2dlemstep  11953  fisumcom2  11957  fsumconst  11973  cvgcmpub  11995  binom  12003  binom1p  12004  binom1dif  12006  bcxmas  12008  divcnv  12016  geo2lim  12035  geoisum  12036  geoisumr  12037  geoisum1  12038  mertenslemi1  12054  mertensabs  12056  prod1dc  12105  fprodconst  12139  fprodcom2fi  12145  efcllem  12178  efcj  12192  efadd  12194  efexp  12201  efgt1p2  12214  tanvalap  12227  tanval2ap  12232  tanval3ap  12233  sinadd  12255  cosadd  12256  dvdsdc  12317  iddvdsexp  12334  dvdsadd  12355  dvds1  12372  odd2np1  12392  oddm1even  12394  m1exp1  12420  divalglemnn  12437  fldivndvdslt  12456  flodddiv4lt  12457  bitsp1  12470  bitsmod  12475  bitsfi  12476  bitscmp  12477  bitsinv1lem  12480  dvdsbnd  12485  gcdnncl  12496  zeqzmulgcd  12499  gcdneg  12511  modgcd  12520  bezoutlemex  12530  bezoutlemeu  12536  dfgcd3  12539  gcdzeq  12551  dvdssq  12560  algrf  12575  eucalgval2  12583  eucalgcvga  12588  lcmval  12593  gcddvdslcm  12603  lcmneg  12604  coprmgcdb  12618  qredeu  12627  divgcdcoprm0  12631  divgcdcoprmex  12632  cncongr1  12633  cncongr2  12634  cncongrcoprm  12636  prmind2  12650  dvdsnprmd  12655  exprmfct  12668  isprm6  12677  pw2dvdslemn  12695  oddpwdclemdc  12703  sqrt2irraplemnn  12709  divnumden  12726  divdenle  12727  nn0sqrtelqelz  12736  phivalfi  12742  crth  12754  eulerth  12763  prmdivdiv  12767  reumodprminv  12784  nnnn0modprm0  12786  nnoddn2prmb  12793  pcval  12827  pcidlem  12854  pcid  12855  pcneg  12856  pc2dvds  12861  pcz  12863  pcprod  12877  prmpwdvds  12886  4sqexercise1  12929  2expltfac  12970  xpct  12975  znnen  12977  ennnfonelemg  12982  ennnfone  13004  ctinfom  13007  ctinf  13009  ssomct  13024  isstruct2im  13050  isstruct2r  13051  setsvalg  13070  setsslnid  13092  ressvalsets  13105  ressex  13106  2strbasg  13161  2stropg  13162  2strbas1g  13164  ressmulrg  13186  ressscag  13224  ressvscag  13225  ressipg  13226  restval  13286  restid2  13289  prdsex  13310  pwsval  13332  qusex  13366  fnpr2o  13380  xpsfval  13389  xpsval  13393  intopsn  13408  mgmidmo  13413  lidrididd  13423  ismnddef  13459  mndinvmod  13486  imasmnd2  13493  ismhm  13502  mhmex  13503  insubm  13526  dfgrp2  13568  grpsubval  13587  grpinvinv  13608  grpsubrcan  13622  grpsubadd  13629  grpaddsubass  13631  grpsubsub4  13634  grppnpcan2  13635  grpnpncan  13636  grpnpncan0  13637  grpnnncan2  13638  dfgrp3m  13640  dfgrp3me  13641  imasgrp2  13655  mhmmnd  13661  mulgfvalg  13666  mulgval  13667  mulgfng  13669  mulg1  13674  mulgnnp1  13675  mulgnndir  13696  mulgass  13704  mulgmodid  13706  issubg2m  13734  grpissubg  13739  isnsg  13747  isnsg3  13752  0nsg  13759  eqgfval  13767  eqger  13769  eqgen  13772  eqgcpbl  13773  quseccl  13778  isghm  13788  kerf1ghm  13819  conjghm  13821  conjsubg  13822  abladdsub  13860  ablpncan3  13862  ablsubsub23  13870  invghm  13874  subgabl  13877  mgpress  13902  rngdi  13911  rnglz  13916  imasrng  13927  srgmulgass  13960  srgrmhm  13965  isring  13971  ringo2times  13999  ringrng  14007  ringlz  14014  imasring  14035  opprrng  14048  opprrngbg  14049  opprring  14050  mulgass3  14056  dvdsrd  14066  dvdsrneg  14075  unitnegcl  14102  dvrvald  14106  dvrid  14109  dvr1  14110  dvrass  14111  dvrdir  14115  ringinvdv  14117  rhmex  14129  isrim0  14133  rhmval  14145  rhmdvdsr  14147  rhmopp  14148  elrhmunit  14149  rhmunitinv  14150  isnzr2  14156  ringelnzr  14159  issubrng2  14182  issubrg2  14213  aprap  14258  lmodvs1  14288  lmod0vs  14293  lmodvs0  14294  lmodvsmmulgdi  14295  lmodfopne  14298  lmodvneg1  14302  lss1  14334  islss3  14351  lsslss  14353  lss1d  14355  lspf  14361  lspsn  14388  lspsnneg  14392  sraval  14409  sraring  14421  qus1  14498  qusrhm  14500  cnfldui  14561  dvdsrzring  14575  mulgghm2  14580  mulgrhm  14581  znval  14608  znf1o  14623  psrbagfi  14645  psrplusgg  14650  mplgrpfi  14678  eltg2b  14736  difopn  14790  ntrcls0  14813  neii1  14829  restbasg  14850  resttopon  14853  restuni2  14859  cnrest2r  14919  tx1cn  14951  txcnp  14953  txcn  14957  txswaphmeo  15003  psmettri  15012  xmeteq0  15041  xmettri  15054  metrtri  15059  ssblex  15113  xmeter  15118  isxms2  15134  cnbl0  15216  cnblcld  15217  reopnap  15228  tgioo  15236  addcncntoplem  15243  expcn  15251  rescncf  15263  cncfcdm  15264  mulc1cncf  15271  cncfcncntop  15275  addccncf  15282  cdivcncfap  15286  negcncf  15287  cnopnap  15293  suplociccex  15307  hoverlt1  15331  hovergt0  15332  dich0  15334  limccl  15341  ellimc3apf  15342  cnplimcim  15349  limccnp2lem  15358  reldvg  15361  dvbsssg  15368  dvcjbr  15390  dvcj  15391  dvfre  15392  dvrecap  15395  dvef  15409  plyaddcl  15436  plymulcl  15437  plysubcl  15438  plyrecj  15445  reeff1olem  15453  pilem3  15465  ptolemy  15506  rplogcl  15561  rpcxpef  15576  cxprec  15592  rpcxproot  15596  rplogb1  15630  logbgt0b  15648  logbgcd1irr  15649  binom4  15661  wilthlem1  15662  sgmnncl  15670  dvdsppwf1o  15671  mersenne  15679  lgslem4  15690  lgsval  15691  lgsval2lem  15697  lgsval4a  15709  lgsdir2lem3  15717  lgsdir2  15720  lgsne0  15725  lgsprme0  15729  lgsmulsqcoprm  15733  gausslemma2dlem0a  15736  gausslemma2dlem1a  15745  2lgslem1b  15776  2lgslem2  15779  2lgsoddprm  15800  struct2slots2dom  15847  structvtxval  15848  structiedg0val  15849  struct2griedg  15855  edgstruct  15872  uhgr0vb  15892  incistruhgr  15898  umgrvad2edg  16017  uspgredg2vlem  16026  uspgredg2v  16027  usgredg2v  16030  ushgredgedg  16032  ushgredgedgloop  16034  wksfval  16043  wlkpropg  16045  uspgr2wlkeq2  16087  uspgr2wlkeqi  16088  upgr2wlkdc  16096  bj-nnan  16124  bj-indind  16319  bj-omtrans  16343  bj-inf2vnlem1  16357  sscoll2  16375  2omap  16388  pw1map  16390  pwtrufal  16392  sssneq  16397  pw1nct  16398  nninfsellemsuc  16408  nninfomnilem  16414  nnnninfex  16418  exmidsbthrlem  16420  qdencn  16425  trilpo  16441  trirec0  16442  apdiff  16446  iswomninnlem  16447  iswomni0  16449  redcwlpo  16453  redc0  16455  reap0  16456  cndcap  16457  dceqnconst  16458  dcapnconst  16459  neapmkv  16466  neap0mkv  16467