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  393  adantlr  481  adantrr  483  adantllr  485  adantlrr  487  adantrlr  489  adantrrr  491  simplll  539  simplrl  541  simprll  543  simprrl  545  anabs1  578  jcab  611  pm4.38  613  pm5.21  707  ioran  764  pm3.14  765  pm4.44  791  ordi  828  pm4.39  834  animorl  835  animorlr  837  pm5.16  840  pm5.54dc  930  intnanr  942  intnanrd  944  dcan  946  dedlema  982  dedlemb  983  pm4.42r  984  prlem2  987  ifpdc  992  dfifp2dc  994  simp1l  1052  simp2l  1054  simp3l  1056  3anandis  1388  xordc1  1442  anxordi  1449  falantru  1452  19.26  1534  exsimpl  1670  sbequ2  1822  sbcof2  1863  sbequilem  1891  sbequ8  1900  euan  2143  mooran1  2159  eupickbi  2169  2exeu  2179  dimatis  2204  rexim  2644  r19.26  2677  r19.40  2705  rspcime  2937  rr19.28v  2966  elrab3t  2981  eueq3dc  3000  mosubt  3003  reu6  3015  sbc2iegf  3122  sbcralt  3128  sbcrext  3129  rmob  3145  csbiebt  3187  ssab2  3332  difdif  3354  uneqin  3482  indifdir  3487  undif3ss  3492  abanssl  3501  rexm  3627  eqifdc  3677  ifandc  3681  ifnebibdc  3686  difsn  3850  opprc1  3924  unissel  3962  ssmin  3987  abssexg  4317  undifexmid  4328  pwntru  4334  exmidundif  4341  exmidundifim  4342  opelopabsb  4400  elopabran  4424  sess1  4480  ordelord  4524  onin  4529  suctr  4564  abnexg  4590  ifexg  4629  ordtriexmidlem  4664  ordtri2or2exmid  4716  ontri2orexmidim  4717  tfi  4727  peano1  4739  peano2  4740  nnpredcl  4768  0nelxp  4800  0nelelxp  4801  brab2a  4826  mosubopt  4838  posng  4845  opabssxp  4847  ideqg  4929  relssres  5099  trin2  5177  dminss  5200  iota4an  5356  iota2  5365  iotam  5367  fununfun  5422  fun11uni  5449  imadiflem  5458  funimaexg  5463  fneq12  5472  fvelrnb  5747  dffo4  5850  ffnfv  5860  ffvresb  5865  fmptco  5868  fcoconst  5873  funopsn  5885  fndmexb  5932  mptmex  5939  fcof1  5983  isotr  6016  isopolem  6022  f1oiso  6026  acexmidlemcase  6074  ovprc1  6116  fnoprabg  6183  elovmporab  6283  elovmporab1w  6284  uchoice  6365  op1steq  6407  dmmpog  6439  1stconst  6451  f1o2ndf1  6458  suppfnss  6491  suppssfvg  6497  brtpos2  6516  tpostpos  6529  tposf12  6534  smores  6557  tfrlemi1  6597  tfr1onlembfn  6609  tfri1dALT  6616  tfrcllembfn  6622  freceq1  6657  freceq2  6658  frectfr  6665  omv2  6732  omsuc  6739  nnsucelsuc  6758  nntri3  6764  nnaordi  6775  nnmordi  6783  nnm00  6797  ecexr  6806  ertr  6816  swoer  6829  erth  6847  ecelqsdm  6873  iinerm  6875  ecinxp  6878  erovlem  6895  pmresg  6951  resixp  7009  elixpsn  7011  mapsnf1o  7013  dom3  7056  modom  7102  mapdom1g  7141  ssenen  7146  phpelm  7162  finexdc  7201  exmidpweq  7210  nnwetri  7217  fiintim  7232  infidc  7242  suppeqfsuppbi  7289  ssfii  7302  fiss  7305  dcfi  7309  2omap  7312  supubti  7333  supisoex  7343  ordiso2  7369  inl11  7399  omp1eomlem  7428  nnnninf  7460  nninfisol  7467  ctssexmid  7484  ismkvnex  7489  omniwomnimkv  7501  nninfwlpor  7508  nninfwlpoim  7513  nninfinfwlpo  7514  en2eleq  7541  en2other2  7542  exmidfodomrlemr  7548  exmidfodomrlemrALT  7549  acnrcl  7551  exmidaclem  7558  djuen  7561  djudoml  7569  netap  7614  2omotaplemst  7618  exmidapne  7620  cc1  7625  acnccim  7632  dmaddpqlem  7738  distrnqg  7748  ltanqi  7763  ltmnqi  7764  ltaddnq  7768  ltrnqg  7781  ltnnnq  7784  enq0sym  7793  addnq0mo  7808  mulnq0mo  7809  addnnnq0  7810  distrnq0  7820  prarloclemn  7860  prarloc  7864  ltdfpr  7867  genplt2i  7871  addnqprl  7890  addnqpru  7891  nqprl  7912  appdivnq  7924  1idprl  7951  1idpru  7952  ltexpri  7974  recexpr  7999  cauappcvgprlemdisj  8012  archrecpr  8025  addsrmo  8104  mulsrmo  8105  addsrpr  8106  mulsrpr  8107  0idsr  8128  1idsr  8129  archsr  8143  prsradd  8147  prsrlt  8148  caucvgsr  8163  map2psrprg  8166  elrealeu  8190  muladd11r  8476  negeu  8511  pncan  8526  pncan3  8528  negsub  8568  addid0  8693  addeq0  8697  posdif  8777  ltnegcon1  8785  subge0  8797  suble0  8798  lesub0  8801  reapval  8898  reapneg  8919  ap0gt0  8962  aprcl  8968  lt0ap0  8970  recextlem1  8973  recapb  8995  div0ap  9026  recrecap  9033  rec11ap  9034  recgt0  9174  mulgt1  9187  lerec2  9213  recp1lt1  9223  recreclt  9224  ledivp1  9227  negiso  9279  nnsub  9326  avglt1  9527  nnrecl  9544  nnnn0addcl  9576  elnn0nn  9588  fcdmnn0fsuppg  9601  nn0ge2m1nn  9610  zaddcl  9667  eluzmn  9911  eluzadd  9934  infregelbex  9981  divfnzn  10004  qaddcl  10018  qreccl  10025  cnref1o  10034  ge0p1rp  10069  divlt1lt  10108  divle1le  10109  addlelt  10152  xrre3  10207  xltnegi  10220  xaddval  10230  xaddcom  10246  xnegdi  10253  xposdif  10267  ixxssixx  10287  iccshftr  10379  iccshftl  10381  iccdil  10383  icccntr  10385  zltaddlt1le  10393  elfz2  10401  peano2fzr  10424  fzdcel  10427  fzsplit2  10438  fzaddel  10448  fzrev2  10475  fzrev2i  10476  fzrev3  10477  elfz1b  10480  fseq1p1m1  10484  uzsubfz0  10519  fzosubel3  10597  eluzgtdifelfzo  10598  fzofzp1b  10629  elfzomelpfzo  10632  exfzdc  10642  fvinim0ffz  10643  zsupcllemex  10646  infssuzcldc  10651  exbtwnzlemshrink  10666  qbtwnz  10669  qbtwnxr  10675  ico0  10679  elicore  10684  xqltnle  10685  apbtwnz  10692  flqge  10700  flqlt  10701  flqltnz  10705  flqbi2  10709  flqaddz  10715  flqmulnn0  10717  intfracq  10740  flqdiv  10741  q0mod  10775  q1mod  10776  mulp1mod1  10785  q2txmodxeq0  10804  modfzo0difsn  10815  frec2uzuzd  10822  frec2uzltd  10823  frec2uzrand  10825  uzennn  10856  seqfveq2g  10897  seq3split  10908  seqsplitg  10909  seq3caopr  10915  seqcaoprg  10916  seqf1oglem2  10940  seqf1og  10941  exp3vallem  10960  exp3val  10961  expnnval  10962  exp1  10965  expcl2lemap  10971  rpexpcl  10978  expnegzap  10993  mulexp  10998  mulexpzap  10999  leexp2r  11013  leexp1a  11014  sq11  11032  subsq  11066  binom2  11071  binom3  11077  zesq  11079  bernneq  11081  sq11ap  11128  zzlesq  11129  mulsubdivbinom2ap  11132  apexp1  11139  facwordi  11161  facubnd  11166  facavg  11167  bcval  11170  bcval5  11184  hashennn  11202  fihashf1rn  11210  fseq1hash  11224  hashdifsn  11243  hashdifpr  11244  hashxp  11250  hashmap  11251  fiubz  11255  fiubnn  11256  fnfz0hash  11258  ffzo0hash  11260  ssenneg  11263  hashfibclem  11265  hashf1  11270  hash2en  11278  wrdval  11290  ffz0iswrdnn0  11314  wrdsymb0  11320  ccatsymb  11353  ccatval21sw  11356  lswccatn0lsw  11362  ccatalpha  11364  ccatrcl1  11365  s111  11382  ccat1st1st  11392  lswccats1fst  11395  swrdlen2  11417  swrdfv2  11418  swrdsbslen  11421  swrds1  11423  ccatswrd  11425  pfxval  11429  pfxclg  11433  pfxmpt  11435  pfxid  11441  pfxfv0  11447  pfxtrcfv0  11449  pfxfvlsw  11450  pfxeq  11451  ccatpfx  11456  swrdpfx  11462  lenrevpfxcctswrd  11467  wrdeqs1cat  11475  cats1un  11476  swrdccatin1  11480  pfxccatin12lem2a  11482  pfxccatin12lem1  11483  pfxccatin12lem3  11487  pfxccatin12  11488  swrdccat  11490  pfxccat3a  11493  swrdccat3blem  11494  swrdccat3b  11495  reuccatpfxs1lem  11501  reuccatpfxs1  11502  s2cl  11540  s2fv0g  11542  shftfvalg  11566  ovshftex  11567  shftdm  11570  shftfib  11571  shftval  11573  shftf  11578  crre  11605  cjexp  11641  cjreim2  11653  uzin2  11736  rexuz3  11739  resqrexlemgt0  11769  resqrex  11775  sqrtgt0  11783  sqrtsq  11793  sqrtmsq  11794  absrpclap  11810  absext  11812  absmul  11818  absid  11820  absexp  11828  nn0abscl  11834  abslt  11837  absle  11838  recvalap  11846  abstri  11853  caubnd2  11866  qdenre  11951  maxabsle  11953  maxabslemval  11957  maxcl  11959  rexanre  11969  min1inf  11981  minabs  11985  minclpr  11986  mul0inf  11990  mingeb  11991  xrmaxiflemcl  11994  xrnegiso  12011  climconst2  12040  climmpt  12049  climres  12052  climcaucn  12100  sumeq1  12104  summodclem2a  12131  isumz  12139  fisumss  12142  fsumzcl2  12155  sumsnf  12159  isumclim3  12173  fsum2dlemstep  12184  fisumcom2  12188  fsumconst  12204  cvgcmpub  12226  binom  12234  binom1p  12235  binom1dif  12237  bcxmas  12239  divcnv  12247  geo2lim  12266  geoisum  12267  geoisumr  12268  geoisum1  12269  mertenslemi1  12285  mertensabs  12287  prod1dc  12336  fprodconst  12370  fprodcom2fi  12376  efcllem  12409  efcj  12423  efadd  12425  efexp  12432  efgt1p2  12445  tanvalap  12458  tanval2ap  12463  tanval3ap  12464  sinadd  12486  cosadd  12487  dvdsdc  12548  iddvdsexp  12565  dvdsadd  12586  dvds1  12603  odd2np1  12623  oddm1even  12625  m1exp1  12651  divalglemnn  12668  fldivndvdslt  12687  flodddiv4lt  12688  bitsp1  12701  bitsmod  12706  bitsfi  12707  bitscmp  12708  bitsinv1lem  12711  dvdsbnd  12716  gcdnncl  12727  zeqzmulgcd  12730  gcdneg  12742  modgcd  12751  bezoutlemex  12761  bezoutlemeu  12767  dfgcd3  12770  gcdzeq  12782  dvdssq  12791  algrf  12806  eucalgval2  12814  eucalgcvga  12819  lcmval  12824  gcddvdslcm  12834  lcmneg  12835  coprmgcdb  12849  qredeu  12858  divgcdcoprm0  12862  divgcdcoprmex  12863  cncongr1  12864  cncongr2  12865  cncongrcoprm  12867  prmind2  12881  dvdsnprmd  12886  exprmfct  12899  isprm6  12908  pw2dvdslemn  12926  oddpwdclemdc  12934  sqrt2irraplemnn  12940  divnumden  12957  divdenle  12958  nn0sqrtelqelz  12967  phivalfi  12973  crth  12985  eulerth  12994  prmdivdiv  12998  reumodprminv  13015  nnnn0modprm0  13017  nnoddn2prmb  13024  pcval  13058  pcidlem  13085  pcid  13086  pcneg  13087  pc2dvds  13092  pcz  13094  pcprod  13108  prmpwdvds  13117  4sqexercise1  13160  2expltfac  13201  ballotfilemfval  13212  ballotfilemefi  13220  ballotfilemodife  13223  ballotfilem4  13224  ballotfilemsval  13235  ballotfilemieq  13243  ballotfilemrv  13246  ballotfilemrinv0  13259  xpct  13270  znnen  13272  ennnfonelemg  13277  ennnfone  13299  ctinfom  13302  ctinf  13304  ssomct  13319  isstruct2im  13345  isstruct2r  13346  setsvalg  13365  setsslnid  13387  ressvalsets  13401  ressex  13402  2strbasg  13457  2stropg  13458  2strbas1g  13460  ressmulrg  13482  ressscag  13520  ressvscag  13521  ressipg  13522  restval  13582  restid2  13585  qusex  13629  fnpr2o  13643  xpsfval  13652  intopsn  13670  mgmidmo  13675  lidrididd  13685  ismnddef  13714  mndinvmod  13741  imasmnd2  13742  ismhm  13751  mhmex  13752  insubm  13775  dfgrp2  13815  grpsubval  13834  grpinvinv  13855  grpsubrcan  13869  grpsubadd  13876  grpaddsubass  13878  grpsubsub4  13881  grppnpcan2  13882  grpnpncan  13883  grpnpncan0  13884  grpnnncan2  13885  dfgrp3m  13887  dfgrp3me  13888  imasgrp2  13896  mhmmnd  13902  mulgfvalg  13907  mulgval  13908  mulgfng  13910  mulg1  13915  mulgnnp1  13916  mulgnndir  13937  mulgass  13945  mulgmodid  13947  issubg2m  13975  grpissubg  13980  isnsg  13988  isnsg3  13993  0nsg  14000  eqgfval  14008  eqger  14010  eqgen  14013  eqgcpbl  14014  quseccl  14019  isghm  14029  kerf1ghm  14060  conjghm  14062  conjsubg  14063  abladdsub  14102  ablpncan3  14104  ablsubsub23  14112  invghm  14116  subgabl  14119  prdsex  14155  xpsval  14184  pwsval  14187  mgpress  14213  rngdi  14222  rnglz  14227  imasrng  14238  srgmulgass  14276  srgrmhm  14281  isring  14287  ringo2times  14316  ringrng  14324  ringlz  14331  imasring  14352  opprrng  14365  opprrngbg  14366  opprring  14367  mulgass3  14374  dvdsrd  14384  dvdsrneg  14393  unitnegcl  14420  dvrvald  14424  dvrid  14427  dvr1  14428  dvrass  14429  dvrdir  14433  ringinvdv  14435  rhmex  14447  isrim0  14451  rhmval  14463  rhmdvdsr  14465  rhmopp  14466  elrhmunit  14467  rhmunitinv  14468  isnzr2  14474  ringelnzr  14477  issubrng2  14501  issubrg2  14532  ringunitap  14576  aprap  14581  aprnzr  14582  opprdrng  14603  lmodvs1  14636  lmod0vs  14641  lmodvs0  14642  lmodvsmmulgdi  14643  lmodfopne  14646  lmodvneg1  14650  lss1  14682  islss3  14699  lsslss  14701  lss1d  14703  lspf  14709  lspsn  14736  lspsnneg  14740  sraval  14757  sraring  14769  qus1  14846  qusrhm  14848  cnfldui  14907  dvdsrzring  14921  mulgghm2  14926  mulgrhm  14927  znval  14954  znf1o  14969  assa2ass  14992  assa2ass2  14993  issubassa3  14995  assamulgscmlem2  15025  psrbagfi  15042  psrbagconcl  15046  psrplusgg  15052  mplgrpfi  15080  eltg2b  15138  difopn  15192  ntrcls0  15215  neii1  15231  restbasg  15252  resttopon  15255  restuni2  15261  cnrest2r  15321  tx1cn  15353  txcnp  15355  txcn  15359  txswaphmeo  15405  psmettri  15414  xmeteq0  15443  xmettri  15456  metrtri  15461  ssblex  15515  xmeter  15520  isxms2  15536  cnbl0  15618  cnblcld  15619  reopnap  15630  tgioo  15638  addcncntoplem  15645  expcn  15653  rescncf  15665  cncfcdm  15666  mulc1cncf  15673  cncfcncntop  15677  addccncf  15684  cdivcncfap  15688  negcncf  15689  cnopnap  15695  suplociccex  15709  hoverlt1  15733  hovergt0  15734  dich0  15736  limccl  15743  ellimc3apf  15744  cnplimcim  15751  limccnp2lem  15760  reldvg  15763  dvbsssg  15770  dvcjbr  15792  dvcj  15793  dvfre  15794  dvrecap  15797  dvef  15811  plyaddcl  15838  plymulcl  15839  plysubcl  15840  plyrecj  15847  reeff1olem  15855  pilem3  15867  ptolemy  15908  rplogcl  15963  rpcxpef  15979  cxprec  15995  rpcxproot  15999  rplogb1  16033  logbgt0b  16051  logbgcd1irr  16052  binom4  16064  birthdaylem1g  16070  wilthlem1  16077  sgmnncl  16085  dvdsppwf1o  16086  mersenne  16094  lgslem4  16105  lgsval  16106  lgsval2lem  16112  lgsval4a  16124  lgsdir2lem3  16132  lgsdir2  16135  lgsne0  16140  lgsprme0  16144  lgsmulsqcoprm  16148  gausslemma2dlem0a  16151  gausslemma2dlem1a  16160  2lgslem1b  16191  2lgslem2  16194  2lgsoddprm  16215  struct2slots2dom  16262  structvtxval  16263  structiedg0val  16264  struct2griedg  16270  edgstruct  16288  uhgr0vb  16308  incistruhgr  16314  umgrvad2edg  16435  uspgredg2vlem  16444  uspgredg2v  16445  usgredg2v  16448  ushgredgedg  16450  ushgredgedgloop  16452  usgr0vb  16457  uhgr0vusgr  16462  edg0usgr  16471  subupgr  16497  upgrspanop  16507  umgrspanop  16508  usgrspanop  16509  vtxdgfval  16512  wksfval  16546  wlkpropg  16548  uspgr2wlkeq2  16590  uspgr2wlkeqi  16591  upgr2wlkdc  16601  trlsex  16611  clwwlkccatlem  16624  clwwlkng  16629  clwwlkext2edg  16646  clwwlknccat  16647  umgr2cwwkdifex  16649  clwwlknonel  16656  clwwlknonccat  16657  clwwlknonex2lem2  16662  clwwlknun  16665  eupthsg  16669  eupth2lem3lem6fi  16695  dichmul0orlem7  16742  dichmul0or  16743  bj-nnan  16747  bj-indind  16941  bj-omtrans  16965  bj-inf2vnlem1  16979  sscoll2  16997  pw1map  17008  pwtrufal  17010  sssneq  17015  pw1nct  17016  exmidnotnotr  17018  nninfsellemsuc  17029  nninfomnilem  17035  nnnninfex  17039  exmidsbthrlem  17041  qdencn  17046  trilpo  17066  trirec0  17067  apdiff  17071  iswomninnlem  17073  iswomni0  17075  redcwlpo  17079  redc0  17081  reap0  17082  cndcap  17083  dceqnconst  17084  dcapnconst  17085  neapmkv  17092  neap0mkv  17093  als-no-surprise  17121