Theorem simpl 108

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 105	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-ia1 105

This theorem is referenced by:  simpli  110  simpld  111  imp  123  adantrd  277  iba  298  pm3.41  329  pm4.45im  332  anim12  342  pm4.71  387  adantlr  469  adantrr  471  adantllr  473  adantlrr  475  adantrlr  477  adantrrr  479  simplll  523  simplrl  525  simprll  527  simprrl  529  anabs1  562  jcab  593  pm4.38  595  pm5.21  685  ioran  742  pm3.14  743  pm4.44  769  ordi  806  pm4.39  812  animorl  813  animorlr  815  pm5.16  818  pm5.54dc  908  intnanr  920  intnanrd  922  dcan  923  dedlema  959  dedlemb  960  pm4.42r  961  prlem2  964  simp1l  1011  simp2l  1013  simp3l  1015  3anandis  1337  xordc1  1383  anxordi  1390  falantru  1393  19.26  1469  exsimpl  1605  sbequ2  1757  sbcof2  1798  sbequilem  1826  sbequ8  1835  euan  2070  mooran1  2086  eupickbi  2096  2exeu  2106  dimatis  2131  rexim  2560  r19.26  2592  r19.40  2620  rspcime  2837  rr19.28v  2866  elrab3t  2881  eueq3dc  2900  mosubt  2903  reu6  2915  sbc2iegf  3021  sbcralt  3027  sbcrext  3028  rmob  3043  csbiebt  3084  ssab2  3226  difdif  3247  uneqin  3373  indifdir  3378  undif3ss  3383  rexm  3508  eqifdc  3554  ifandc  3557  difsn  3710  opprc1  3780  unissel  3818  ssmin  3843  abssexg  4161  undifexmid  4172  pwntru  4178  exmidundif  4185  exmidundifim  4186  opelopabsb  4238  sess1  4315  ordelord  4359  onin  4364  suctr  4399  abnexg  4424  ordtriexmidlem  4496  ordtri2or2exmid  4548  ontri2orexmidim  4549  tfi  4559  peano1  4571  peano2  4572  nnpredcl  4600  0nelxp  4632  0nelelxp  4633  brab2a  4657  mosubopt  4669  posng  4676  opabssxp  4678  ideqg  4755  relssres  4922  trin2  4995  dminss  5018  iota4an  5172  iota2  5179  fun11uni  5258  imadiflem  5267  funimaexg  5272  fneq12  5281  fvelrnb  5534  dffo4  5633  ffnfv  5643  ffvresb  5648  fmptco  5651  fcoconst  5656  fcof1  5751  isotr  5784  isopolem  5790  f1oiso  5794  acexmidlemcase  5837  ovprc1  5878  fnoprabg  5943  op1steq  6147  dmmpog  6177  1stconst  6189  f1o2ndf1  6196  brtpos2  6219  tpostpos  6232  tposf12  6237  smores  6260  tfrlemi1  6300  tfr1onlembfn  6312  tfri1dALT  6319  tfrcllembfn  6325  freceq1  6360  freceq2  6361  frectfr  6368  omv2  6433  omsuc  6440  nnsucelsuc  6459  nntri3  6465  nnaordi  6476  nnmordi  6484  nnm00  6497  ecexr  6506  ertr  6516  swoer  6529  erth  6545  ecelqsdm  6571  iinerm  6573  ecinxp  6576  erovlem  6593  pmresg  6642  resixp  6699  elixpsn  6701  mapsnf1o  6703  dom3  6742  mapdom1g  6813  ssenen  6817  phpelm  6832  finexdc  6868  exmidpweq  6875  nnwetri  6881  fiintim  6894  ssfii  6939  fiss  6942  dcfi  6946  supubti  6964  supisoex  6974  ordiso2  7000  inl11  7030  omp1eomlem  7059  nnnninf  7090  nninfisol  7097  ctssexmid  7114  ismkvnex  7119  omniwomnimkv  7131  en2eleq  7151  en2other2  7152  exmidfodomrlemr  7158  exmidfodomrlemrALT  7159  exmidaclem  7164  djuen  7167  djudoml  7175  cc1  7206  dmaddpqlem  7318  distrnqg  7328  ltanqi  7343  ltmnqi  7344  ltaddnq  7348  ltrnqg  7361  ltnnnq  7364  enq0sym  7373  addnq0mo  7388  mulnq0mo  7389  addnnnq0  7390  distrnq0  7400  prarloclemn  7440  prarloc  7444  ltdfpr  7447  genplt2i  7451  addnqprl  7470  addnqpru  7471  nqprl  7492  appdivnq  7504  1idprl  7531  1idpru  7532  ltexpri  7554  recexpr  7579  cauappcvgprlemdisj  7592  archrecpr  7605  addsrmo  7684  mulsrmo  7685  addsrpr  7686  mulsrpr  7687  0idsr  7708  1idsr  7709  archsr  7723  prsradd  7727  prsrlt  7728  caucvgsr  7743  map2psrprg  7746  elrealeu  7770  muladd11r  8054  negeu  8089  pncan  8104  pncan3  8106  negsub  8146  addid0  8271  posdif  8353  ltnegcon1  8361  subge0  8373  suble0  8374  lesub0  8377  reapval  8474  reapneg  8495  ap0gt0  8538  aprcl  8544  lt0ap0  8546  recextlem1  8548  div0ap  8598  recrecap  8605  rec11ap  8606  recgt0  8745  mulgt1  8758  lerec2  8784  recp1lt1  8794  recreclt  8795  ledivp1  8798  negiso  8850  nnsub  8896  avglt1  9095  nnrecl  9112  nnnn0addcl  9144  elnn0nn  9156  nn0ge2m1nn  9174  zaddcl  9231  eluzadd  9494  infregelbex  9536  divfnzn  9559  qaddcl  9573  qreccl  9580  cnref1o  9588  ge0p1rp  9621  divlt1lt  9660  divle1le  9661  addlelt  9704  xrre3  9758  xltnegi  9771  xaddval  9781  xaddcom  9797  xnegdi  9804  xposdif  9818  ixxssixx  9838  iccshftr  9930  iccshftl  9932  iccdil  9934  icccntr  9936  zltaddlt1le  9943  elfz2  9951  peano2fzr  9972  fzdcel  9975  fzsplit2  9985  fzaddel  9994  fzrev2  10020  fzrev2i  10021  fzrev3  10022  elfz1b  10025  fseq1p1m1  10029  uzsubfz0  10064  fzosubel3  10131  eluzgtdifelfzo  10132  fzofzp1b  10163  elfzomelpfzo  10166  exfzdc  10175  fvinim0ffz  10176  exbtwnzlemshrink  10184  qbtwnz  10187  qbtwnxr  10193  ico0  10197  elicore  10202  apbtwnz  10209  flqge  10217  flqlt  10218  flqltnz  10222  flqbi2  10226  flqaddz  10232  flqmulnn0  10234  intfracq  10255  flqdiv  10256  q0mod  10290  q1mod  10291  mulp1mod1  10300  q2txmodxeq0  10319  modfzo0difsn  10330  frec2uzuzd  10337  frec2uzltd  10338  frec2uzrand  10340  uzennn  10371  seq3split  10414  seq3caopr  10418  exp3vallem  10456  exp3val  10457  expnnval  10458  exp1  10461  expcl2lemap  10467  rpexpcl  10474  expnegzap  10489  mulexp  10494  mulexpzap  10495  leexp2r  10509  leexp1a  10510  sq11  10527  subsq  10561  binom2  10566  binom3  10572  zesq  10573  bernneq  10575  sq11ap  10622  apexp1  10631  facwordi  10653  facubnd  10658  facavg  10659  bcval  10662  bcval5  10676  hashennn  10693  fihashf1rn  10702  fseq1hash  10714  hashdifsn  10732  hashdifpr  10733  hashxp  10739  fiubz  10742  fiubnn  10743  fnfz0hash  10745  ffzo0hash  10747  shftfvalg  10760  ovshftex  10761  shftdm  10764  shftfib  10765  shftval  10767  shftf  10772  crre  10799  cjexp  10835  cjreim2  10846  uzin2  10929  rexuz3  10932  resqrexlemgt0  10962  resqrex  10968  sqrtgt0  10976  sqrtsq  10986  sqrtmsq  10987  absrpclap  11003  absext  11005  absmul  11011  absid  11013  absexp  11021  nn0abscl  11027  abslt  11030  absle  11031  recvalap  11039  abstri  11046  caubnd2  11059  qdenre  11144  maxabsle  11146  maxabslemval  11150  maxcl  11152  rexanre  11162  min1inf  11173  minabs  11177  minclpr  11178  mul0inf  11182  mingeb  11183  xrmaxiflemcl  11186  xrnegiso  11203  climconst2  11232  climmpt  11241  climres  11244  climcaucn  11292  sumeq1  11296  summodclem2a  11322  isumz  11330  fisumss  11333  fsumzcl2  11346  sumsnf  11350  isumclim3  11364  fsum2dlemstep  11375  fisumcom2  11379  fsumconst  11395  cvgcmpub  11417  binom  11425  binom1p  11426  binom1dif  11428  bcxmas  11430  divcnv  11438  geo2lim  11457  geoisum  11458  geoisumr  11459  geoisum1  11460  mertenslemi1  11476  mertensabs  11478  prod1dc  11527  fprodconst  11561  fprodcom2fi  11567  efcllem  11600  efcj  11614  efadd  11616  efexp  11623  efgt1p2  11636  tanvalap  11649  tanval2ap  11654  tanval3ap  11655  sinadd  11677  cosadd  11678  dvdsdc  11738  iddvdsexp  11755  dvdsadd  11776  dvds1  11791  odd2np1  11810  oddm1even  11812  m1exp1  11838  divalglemnn  11855  fldivndvdslt  11872  flodddiv4lt  11873  zsupcllemex  11879  infssuzcldc  11884  dvdsbnd  11889  gcdnncl  11900  zeqzmulgcd  11903  gcdneg  11915  modgcd  11924  bezoutlemex  11934  bezoutlemeu  11940  dfgcd3  11943  gcdzeq  11955  dvdssq  11964  algrf  11977  eucalgval2  11985  eucalgcvga  11990  lcmval  11995  gcddvdslcm  12005  lcmneg  12006  coprmgcdb  12020  qredeu  12029  divgcdcoprm0  12033  divgcdcoprmex  12034  cncongr1  12035  cncongr2  12036  cncongrcoprm  12038  prmind2  12052  dvdsnprmd  12057  exprmfct  12070  isprm6  12079  pw2dvdslemn  12097  oddpwdclemdc  12105  sqrt2irraplemnn  12111  divnumden  12128  divdenle  12129  nn0sqrtelqelz  12138  phivalfi  12144  crth  12156  eulerth  12165  prmdivdiv  12169  reumodprminv  12185  nnnn0modprm0  12187  nnoddn2prmb  12194  pcval  12228  pcidlem  12254  pcid  12255  pcneg  12256  pc2dvds  12261  pcz  12263  pcprod  12276  prmpwdvds  12285  xpct  12329  znnen  12331  ennnfonelemg  12336  ennnfone  12358  ctinfom  12361  ctinf  12363  ssomct  12378  isstruct2im  12404  isstruct2r  12405  setsvalg  12424  setsslnid  12445  ressid2  12454  ressval2  12455  2strbasg  12496  2stropg  12497  2strbas1g  12499  restval  12562  restid2  12565  intopsn  12598  mgmidmo  12603  lidrididd  12613  eltg2b  12694  difopn  12748  ntrcls0  12771  neii1  12787  restbasg  12808  resttopon  12811  restuni2  12817  cnrest2r  12877  tx1cn  12909  txcnp  12911  txcn  12915  txswaphmeo  12961  psmettri  12970  xmeteq0  12999  xmettri  13012  metrtri  13017  ssblex  13071  xmeter  13076  isxms2  13092  cnbl0  13174  cnblcld  13175  reopnap  13178  tgioo  13186  addcncntoplem  13191  rescncf  13208  cncffvrn  13209  mulc1cncf  13216  cncfcncntop  13220  addccncf  13226  cdivcncfap  13227  negcncf  13228  cnopnap  13234  suplociccex  13243  limccl  13268  ellimc3apf  13269  cnplimcim  13276  limccnp2lem  13285  reldvg  13288  dvbsssg  13295  dvcjbr  13312  dvcj  13313  dvfre  13314  dvrecap  13317  dvef  13328  reeff1olem  13332  pilem3  13344  ptolemy  13385  rplogcl  13440  rpcxpef  13455  cxprec  13471  rpcxproot  13474  rplogb1  13506  logbgt0b  13524  logbgcd1irr  13525  binom4  13537  lgslem4  13544  lgsval  13545  lgsval2lem  13551  lgsval4a  13563  lgsdir2lem3  13571  lgsdir2  13574  lgsne0  13579  lgsprme0  13583  lgsmulsqcoprm  13587  bj-nnan  13617  bj-indind  13814  bj-omtrans  13838  bj-inf2vnlem1  13852  sscoll2  13870  pwtrufal  13877  sssneq  13882  pw1nct  13883  nninfsellemsuc  13892  nninfomnilem  13898  exmidsbthrlem  13901  qdencn  13906  trilpo  13922  trirec0  13923  apdiff  13927  iswomninnlem  13928  iswomni0  13930  redcwlpo  13934  redc0  13936  reap0  13937  dceqnconst  13938  dcapnconst  13939  neapmkv  13946