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  8446  negeu  8481  pncan  8496  pncan3  8498  negsub  8538  addid0  8663  addeq0  8667  posdif  8747  ltnegcon1  8755  subge0  8767  suble0  8768  lesub0  8771  reapval  8868  reapneg  8889  ap0gt0  8932  aprcl  8938  lt0ap0  8940  recextlem1  8943  recapb  8965  div0ap  8996  recrecap  9003  rec11ap  9004  recgt0  9144  mulgt1  9157  lerec2  9183  recp1lt1  9193  recreclt  9194  ledivp1  9197  negiso  9249  nnsub  9296  avglt1  9497  nnrecl  9514  nnnn0addcl  9546  elnn0nn  9558  fcdmnn0fsuppg  9571  nn0ge2m1nn  9580  zaddcl  9637  eluzmn  9881  eluzadd  9904  infregelbex  9951  divfnzn  9974  qaddcl  9988  qreccl  9995  cnref1o  10004  ge0p1rp  10039  divlt1lt  10078  divle1le  10079  addlelt  10122  xrre3  10177  xltnegi  10190  xaddval  10200  xaddcom  10216  xnegdi  10223  xposdif  10237  ixxssixx  10257  iccshftr  10349  iccshftl  10351  iccdil  10353  icccntr  10355  zltaddlt1le  10363  elfz2  10371  peano2fzr  10394  fzdcel  10397  fzsplit2  10407  fzaddel  10417  fzrev2  10444  fzrev2i  10445  fzrev3  10446  elfz1b  10449  fseq1p1m1  10453  uzsubfz0  10488  fzosubel3  10566  eluzgtdifelfzo  10567  fzofzp1b  10598  elfzomelpfzo  10601  exfzdc  10611  fvinim0ffz  10612  zsupcllemex  10615  infssuzcldc  10620  exbtwnzlemshrink  10635  qbtwnz  10638  qbtwnxr  10644  ico0  10648  elicore  10653  xqltnle  10654  apbtwnz  10661  flqge  10669  flqlt  10670  flqltnz  10674  flqbi2  10678  flqaddz  10684  flqmulnn0  10686  intfracq  10709  flqdiv  10710  q0mod  10744  q1mod  10745  mulp1mod1  10754  q2txmodxeq0  10773  modfzo0difsn  10784  frec2uzuzd  10791  frec2uzltd  10792  frec2uzrand  10794  uzennn  10825  seqfveq2g  10866  seq3split  10877  seqsplitg  10878  seq3caopr  10884  seqcaoprg  10885  seqf1oglem2  10909  seqf1og  10910  exp3vallem  10929  exp3val  10930  expnnval  10931  exp1  10934  expcl2lemap  10940  rpexpcl  10947  expnegzap  10962  mulexp  10967  mulexpzap  10968  leexp2r  10982  leexp1a  10983  sq11  11001  subsq  11035  binom2  11040  binom3  11046  zesq  11048  bernneq  11050  sq11ap  11097  zzlesq  11098  mulsubdivbinom2ap  11101  apexp1  11108  facwordi  11130  facubnd  11135  facavg  11136  bcval  11139  bcval5  11153  hashennn  11171  fihashf1rn  11179  fseq1hash  11193  hashdifsn  11212  hashdifpr  11213  hashxp  11219  hashmap  11220  fiubz  11224  fiubnn  11225  fnfz0hash  11227  ffzo0hash  11229  ssenneg  11232  hashfibclem  11234  hash2en  11243  wrdval  11255  ffz0iswrdnn0  11279  wrdsymb0  11285  ccatsymb  11318  ccatval21sw  11321  lswccatn0lsw  11327  ccatalpha  11329  ccatrcl1  11330  s111  11347  ccat1st1st  11357  lswccats1fst  11360  swrdlen2  11382  swrdfv2  11383  swrdsbslen  11386  swrds1  11388  ccatswrd  11390  pfxval  11394  pfxclg  11398  pfxmpt  11400  pfxid  11406  pfxfv0  11412  pfxtrcfv0  11414  pfxfvlsw  11415  pfxeq  11416  ccatpfx  11421  swrdpfx  11427  lenrevpfxcctswrd  11432  wrdeqs1cat  11440  cats1un  11441  swrdccatin1  11445  pfxccatin12lem2a  11447  pfxccatin12lem1  11448  pfxccatin12lem3  11452  pfxccatin12  11453  swrdccat  11455  pfxccat3a  11458  swrdccat3blem  11459  swrdccat3b  11460  reuccatpfxs1lem  11466  reuccatpfxs1  11467  s2cl  11505  s2fv0g  11507  shftfvalg  11531  ovshftex  11532  shftdm  11535  shftfib  11536  shftval  11538  shftf  11543  crre  11570  cjexp  11606  cjreim2  11618  uzin2  11701  rexuz3  11704  resqrexlemgt0  11734  resqrex  11740  sqrtgt0  11748  sqrtsq  11758  sqrtmsq  11759  absrpclap  11775  absext  11777  absmul  11783  absid  11785  absexp  11793  nn0abscl  11799  abslt  11802  absle  11803  recvalap  11811  abstri  11818  caubnd2  11831  qdenre  11916  maxabsle  11918  maxabslemval  11922  maxcl  11924  rexanre  11934  min1inf  11946  minabs  11950  minclpr  11951  mul0inf  11955  mingeb  11956  xrmaxiflemcl  11959  xrnegiso  11976  climconst2  12005  climmpt  12014  climres  12017  climcaucn  12065  sumeq1  12069  summodclem2a  12096  isumz  12104  fisumss  12107  fsumzcl2  12120  sumsnf  12124  isumclim3  12138  fsum2dlemstep  12149  fisumcom2  12153  fsumconst  12169  cvgcmpub  12191  binom  12199  binom1p  12200  binom1dif  12202  bcxmas  12204  divcnv  12212  geo2lim  12231  geoisum  12232  geoisumr  12233  geoisum1  12234  mertenslemi1  12250  mertensabs  12252  prod1dc  12301  fprodconst  12335  fprodcom2fi  12341  efcllem  12374  efcj  12388  efadd  12390  efexp  12397  efgt1p2  12410  tanvalap  12423  tanval2ap  12428  tanval3ap  12429  sinadd  12451  cosadd  12452  dvdsdc  12513  iddvdsexp  12530  dvdsadd  12551  dvds1  12568  odd2np1  12588  oddm1even  12590  m1exp1  12616  divalglemnn  12633  fldivndvdslt  12652  flodddiv4lt  12653  bitsp1  12666  bitsmod  12671  bitsfi  12672  bitscmp  12673  bitsinv1lem  12676  dvdsbnd  12681  gcdnncl  12692  zeqzmulgcd  12695  gcdneg  12707  modgcd  12716  bezoutlemex  12726  bezoutlemeu  12732  dfgcd3  12735  gcdzeq  12747  dvdssq  12756  algrf  12771  eucalgval2  12779  eucalgcvga  12784  lcmval  12789  gcddvdslcm  12799  lcmneg  12800  coprmgcdb  12814  qredeu  12823  divgcdcoprm0  12827  divgcdcoprmex  12828  cncongr1  12829  cncongr2  12830  cncongrcoprm  12832  prmind2  12846  dvdsnprmd  12851  exprmfct  12864  isprm6  12873  pw2dvdslemn  12891  oddpwdclemdc  12899  sqrt2irraplemnn  12905  divnumden  12922  divdenle  12923  nn0sqrtelqelz  12932  phivalfi  12938  crth  12950  eulerth  12959  prmdivdiv  12963  reumodprminv  12980  nnnn0modprm0  12982  nnoddn2prmb  12989  pcval  13023  pcidlem  13050  pcid  13051  pcneg  13052  pc2dvds  13057  pcz  13059  pcprod  13073  prmpwdvds  13082  4sqexercise1  13125  2expltfac  13166  ballotfilemfval  13177  ballotfilemefi  13185  ballotfilemodife  13188  ballotfilem4  13189  ballotfilemsval  13200  ballotfilemieq  13208  ballotfilemrv  13211  ballotfilemrinv0  13224  xpct  13235  znnen  13237  ennnfonelemg  13242  ennnfone  13264  ctinfom  13267  ctinf  13269  ssomct  13284  isstruct2im  13310  isstruct2r  13311  setsvalg  13330  setsslnid  13352  ressvalsets  13365  ressex  13366  2strbasg  13421  2stropg  13422  2strbas1g  13424  ressmulrg  13446  ressscag  13484  ressvscag  13485  ressipg  13486  restval  13546  restid2  13549  qusex  13593  fnpr2o  13607  xpsfval  13616  intopsn  13634  mgmidmo  13639  lidrididd  13649  ismnddef  13683  mndinvmod  13710  imasmnd2  13711  ismhm  13720  mhmex  13721  insubm  13744  dfgrp2  13786  grpsubval  13805  grpinvinv  13826  grpsubrcan  13840  grpsubadd  13847  grpaddsubass  13849  grpsubsub4  13852  grppnpcan2  13853  grpnpncan  13854  grpnpncan0  13855  grpnnncan2  13856  dfgrp3m  13858  dfgrp3me  13859  imasgrp2  13867  mhmmnd  13873  mulgfvalg  13878  mulgval  13879  mulgfng  13881  mulg1  13886  mulgnnp1  13887  mulgnndir  13908  mulgass  13916  mulgmodid  13918  issubg2m  13946  grpissubg  13951  isnsg  13959  isnsg3  13964  0nsg  13971  eqgfval  13979  eqger  13981  eqgen  13984  eqgcpbl  13985  quseccl  13990  isghm  14000  kerf1ghm  14031  conjghm  14033  conjsubg  14034  abladdsub  14072  ablpncan3  14074  ablsubsub23  14082  invghm  14086  subgabl  14089  prdsex  14118  xpsval  14147  pwsval  14150  mgpress  14174  rngdi  14183  rnglz  14188  imasrng  14199  srgmulgass  14236  srgrmhm  14241  isring  14247  ringo2times  14275  ringrng  14283  ringlz  14290  imasring  14311  opprrng  14324  opprrngbg  14325  opprring  14326  mulgass3  14333  dvdsrd  14343  dvdsrneg  14352  unitnegcl  14379  dvrvald  14383  dvrid  14386  dvr1  14387  dvrass  14388  dvrdir  14392  ringinvdv  14394  rhmex  14406  isrim0  14410  rhmval  14422  rhmdvdsr  14424  rhmopp  14425  elrhmunit  14426  rhmunitinv  14427  isnzr2  14433  ringelnzr  14436  issubrng2  14460  issubrg2  14491  ringunitap  14535  aprap  14540  aprnzr  14541  opprdrng  14562  lmodvs1  14594  lmod0vs  14599  lmodvs0  14600  lmodvsmmulgdi  14601  lmodfopne  14604  lmodvneg1  14608  lss1  14640  islss3  14657  lsslss  14659  lss1d  14661  lspf  14667  lspsn  14694  lspsnneg  14698  sraval  14715  sraring  14727  qus1  14804  qusrhm  14806  cnfldui  14867  dvdsrzring  14881  mulgghm2  14886  mulgrhm  14887  znval  14914  znf1o  14929  psrbagfi  14953  psrbagconcl  14957  psrplusgg  14963  mplgrpfi  14991  eltg2b  15049  difopn  15103  ntrcls0  15126  neii1  15142  restbasg  15163  resttopon  15166  restuni2  15172  cnrest2r  15232  tx1cn  15264  txcnp  15266  txcn  15270  txswaphmeo  15316  psmettri  15325  xmeteq0  15354  xmettri  15367  metrtri  15372  ssblex  15426  xmeter  15431  isxms2  15447  cnbl0  15529  cnblcld  15530  reopnap  15541  tgioo  15549  addcncntoplem  15556  expcn  15564  rescncf  15576  cncfcdm  15577  mulc1cncf  15584  cncfcncntop  15588  addccncf  15595  cdivcncfap  15599  negcncf  15600  cnopnap  15606  suplociccex  15620  hoverlt1  15644  hovergt0  15645  dich0  15647  limccl  15654  ellimc3apf  15655  cnplimcim  15662  limccnp2lem  15671  reldvg  15674  dvbsssg  15681  dvcjbr  15703  dvcj  15704  dvfre  15705  dvrecap  15708  dvef  15722  plyaddcl  15749  plymulcl  15750  plysubcl  15751  plyrecj  15758  reeff1olem  15766  pilem3  15778  ptolemy  15819  rplogcl  15874  rpcxpef  15889  cxprec  15905  rpcxproot  15909  rplogb1  15943  logbgt0b  15961  logbgcd1irr  15962  binom4  15974  wilthlem1  15978  sgmnncl  15986  dvdsppwf1o  15987  mersenne  15995  lgslem4  16006  lgsval  16007  lgsval2lem  16013  lgsval4a  16025  lgsdir2lem3  16033  lgsdir2  16036  lgsne0  16041  lgsprme0  16045  lgsmulsqcoprm  16049  gausslemma2dlem0a  16052  gausslemma2dlem1a  16061  2lgslem1b  16092  2lgslem2  16095  2lgsoddprm  16116  struct2slots2dom  16163  structvtxval  16164  structiedg0val  16165  struct2griedg  16171  edgstruct  16189  uhgr0vb  16209  incistruhgr  16215  umgrvad2edg  16336  uspgredg2vlem  16345  uspgredg2v  16346  usgredg2v  16349  ushgredgedg  16351  ushgredgedgloop  16353  usgr0vb  16358  uhgr0vusgr  16363  edg0usgr  16372  subupgr  16398  upgrspanop  16408  umgrspanop  16409  usgrspanop  16410  vtxdgfval  16413  wksfval  16447  wlkpropg  16449  uspgr2wlkeq2  16491  uspgr2wlkeqi  16492  upgr2wlkdc  16502  trlsex  16512  clwwlkccatlem  16525  clwwlkng  16530  clwwlkext2edg  16547  clwwlknccat  16548  umgr2cwwkdifex  16550  clwwlknonel  16557  clwwlknonccat  16558  clwwlknonex2lem2  16563  clwwlknun  16566  eupthsg  16570  eupth2lem3lem6fi  16596  dichmul0orlem7  16643  dichmul0or  16644  bj-nnan  16648  bj-indind  16842  bj-omtrans  16866  bj-inf2vnlem1  16880  sscoll2  16898  pw1map  16909  pwtrufal  16911  sssneq  16916  pw1nct  16917  exmidnotnotr  16919  nninfsellemsuc  16930  nninfomnilem  16936  nnnninfex  16940  exmidsbthrlem  16942  qdencn  16947  trilpo  16967  trirec0  16968  apdiff  16972  iswomninnlem  16974  iswomni0  16976  redcwlpo  16980  redc0  16982  reap0  16983  cndcap  16984  dceqnconst  16985  dcapnconst  16986  neapmkv  16993  neap0mkv  16994