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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-ia1 106

This theorem is used 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  3852  opprc1  3926  unissel  3964  ssmin  3989  abssexg  4319  undifexmid  4330  pwntru  4336  exmidundif  4343  exmidundifim  4344  opelopabsb  4402  elopabran  4426  sess1  4482  ordelord  4526  onin  4531  suctr  4566  abnexg  4592  ifexg  4631  ordtriexmidlem  4666  ordtri2or2exmid  4718  ontri2orexmidim  4719  tfi  4729  peano1  4741  peano2  4742  nnpredcl  4770  0nelxp  4802  0nelelxp  4803  brab2a  4828  mosubopt  4840  posng  4847  opabssxp  4849  ideqg  4931  relssres  5101  trin2  5179  dminss  5202  iota4an  5358  iota2  5367  iotam  5369  fununfun  5424  fun11uni  5451  imadiflem  5460  funimaexg  5465  fneq12  5474  fvelrnb  5750  dffo4  5856  ffnfv  5866  ffvresb  5871  fmptco  5874  fcoconst  5879  funopsn  5891  fndmexb  5938  mptmex  5945  fcof1  5989  isotr  6022  isopolem  6028  f1oiso  6032  acexmidlemcase  6080  ovprc1  6122  fnoprabg  6189  elovmporab  6289  elovmporab1w  6290  uchoice  6371  op1steq  6413  dmmpog  6445  1stconst  6457  f1o2ndf1  6464  suppfnss  6497  suppssfvg  6503  brtpos2  6522  tpostpos  6535  tposf12  6540  smores  6563  tfrlemi1  6603  tfr1onlembfn  6615  tfri1dALT  6622  tfrcllembfn  6628  freceq1  6663  freceq2  6664  frectfr  6671  omv2  6738  omsuc  6745  nnsucelsuc  6764  nntri3  6770  nnaordi  6781  nnmordi  6789  nnm00  6803  ecexr  6812  ertr  6822  swoer  6835  erth  6853  ecelqsdm  6879  iinerm  6881  ecinxp  6884  erovlem  6901  pmresg  6957  resixp  7015  elixpsn  7017  mapsnf1o  7019  dom3  7062  modom  7108  mapdom1g  7147  ssenen  7152  phpelm  7168  finexdc  7207  exmidpweq  7216  nnwetri  7223  fiintim  7238  infidc  7248  suppeqfsuppbi  7295  ssfii  7308  fiss  7311  dcfi  7315  2omap  7319  supubti  7340  supisoex  7350  ordiso2  7376  inl11  7406  omp1eomlem  7435  nnnninf  7467  nninfisol  7474  ctssexmid  7491  ismkvnex  7496  omniwomnimkv  7508  nninfwlpor  7515  nninfwlpoim  7520  nninfinfwlpo  7521  en2eleq  7548  en2other2  7549  exmidfodomrlemr  7555  exmidfodomrlemrALT  7556  acnrcl  7558  exmidaclem  7565  djuen  7568  djudoml  7576  netap  7621  2omotaplemst  7625  exmidapne  7627  cc1  7632  acnccim  7639  dmaddpqlem  7745  distrnqg  7755  ltanqi  7770  ltmnqi  7771  ltaddnq  7775  ltrnqg  7788  ltnnnq  7791  enq0sym  7800  addnq0mo  7815  mulnq0mo  7816  addnnnq0  7817  distrnq0  7827  prarloclemn  7867  prarloc  7871  ltdfpr  7874  genplt2i  7878  addnqprl  7897  addnqpru  7898  nqprl  7919  appdivnq  7931  1idprl  7958  1idpru  7959  ltexpri  7981  recexpr  8006  cauappcvgprlemdisj  8019  archrecpr  8032  addsrmo  8111  mulsrmo  8112  addsrpr  8113  mulsrpr  8114  0idsr  8135  1idsr  8136  archsr  8150  prsradd  8154  prsrlt  8155  caucvgsr  8170  map2psrprg  8173  elrealeu  8197  muladd11r  8484  negeu  8519  pncan  8534  pncan3  8536  negsub  8576  addid0  8701  addeq0  8705  posdif  8785  ltnegcon1  8793  subge0  8805  suble0  8806  lesub0  8809  reapval  8907  reapneg  8928  ap0gt0  8971  aprcl  8977  lt0ap0  8979  recextlem1  8982  recapb  9004  div0ap  9035  recrecap  9042  rec11ap  9043  recgt0  9183  mulgt1  9196  lerec2  9222  recp1lt1  9232  recreclt  9233  ledivp1  9236  negiso  9288  nnsub  9346  avglt1  9549  nnrecl  9566  nnnn0addcl  9598  elnn0nn  9610  fcdmnn0fsuppg  9623  nn0ge2m1nn  9632  zaddcl  9689  eluzmn  9938  eluzadd  9961  infregelbex  10008  divfnzn  10031  qaddcl  10045  qreccl  10052  cnref1o  10062  ge0p1rp  10097  divlt1lt  10136  divle1le  10137  addlelt  10180  xrre3  10235  xltnegi  10248  xaddval  10258  xaddcom  10274  xnegdi  10281  xposdif  10295  ixxssixx  10315  iccshftr  10407  iccshftl  10409  iccdil  10411  icccntr  10413  zltaddlt1le  10421  elfz2  10429  peano2fzr  10452  fzdcel  10455  fzsplit2  10466  fzaddel  10476  fzrev2  10503  fzrev2i  10504  fzrev3  10505  elfz1b  10508  fseq1p1m1  10512  uzsubfz0  10547  fzosubel3  10625  eluzgtdifelfzo  10626  fzofzp1b  10657  elfzomelpfzo  10660  exfzdc  10670  fvinim0ffz  10671  zsupcllemex  10674  infssuzcldc  10679  exbtwnzlemshrink  10694  qbtwnz  10697  qbtwnxr  10703  ico0  10707  elicore  10712  xqltnle  10713  apbtwnz  10720  flaplelt  10724  flqge  10730  flapge  10731  flqlt  10732  flqltnz  10736  flqbi2  10740  flqaddz  10746  flqmulnn0  10748  intfracq  10771  flqdiv  10772  q0mod  10806  q1mod  10807  mulp1mod1  10816  q2txmodxeq0  10835  modfzo0difsn  10846  frec2uzuzd  10853  frec2uzltd  10854  frec2uzrand  10856  uzennn  10887  seqfveq2g  10928  seq3split  10939  seqsplitg  10940  seq3caopr  10946  seqcaoprg  10947  seqf1oglem2  10971  seqf1og  10972  exp3vallem  10991  exp3val  10992  expnnval  10993  exp1  10996  expcl2lemap  11002  rpexpcl  11009  expnegzap  11024  mulexp  11029  mulexpzap  11030  leexp2r  11044  leexp1a  11045  sq11  11063  subsq  11097  binom2  11102  binom3  11108  zesq  11110  bernneq  11112  sq11ap  11159  zzlesq  11160  mulsubdivbinom2ap  11164  apexp1  11171  facwordi  11193  facubnd  11198  facavg  11199  bcval  11202  bcval5  11216  hashennn  11234  fihashf1rn  11242  fseq1hash  11256  hashdifsn  11275  hashdifpr  11276  hashxp  11282  hashmap  11283  fiubz  11287  fiubnn  11288  fnfz0hash  11290  ffzo0hash  11292  ssenneg  11295  hashfibclem  11297  hashf1  11302  hash2en  11310  wrdval  11322  ffz0iswrdnn0  11346  wrdsymb0  11352  ccatsymb  11385  ccatval21sw  11388  lswccatn0lsw  11394  ccatalpha  11396  ccatrcl1  11397  s111  11414  ccat1st1st  11424  lswccats1fst  11427  swrdlen2  11449  swrdfv2  11450  swrdsbslen  11453  swrds1  11455  ccatswrd  11457  pfxval  11461  pfxclg  11465  pfxmpt  11467  pfxid  11473  pfxfv0  11479  pfxtrcfv0  11481  pfxfvlsw  11482  pfxeq  11483  ccatpfx  11488  swrdpfx  11494  lenrevpfxcctswrd  11499  wrdeqs1cat  11507  cats1un  11508  swrdccatin1  11512  pfxccatin12lem2a  11514  pfxccatin12lem1  11515  pfxccatin12lem3  11519  pfxccatin12  11520  swrdccat  11522  pfxccat3a  11525  swrdccat3blem  11526  swrdccat3b  11527  reuccatpfxs1lem  11533  reuccatpfxs1  11534  s2cl  11572  s2fv0g  11574  shftfvalg  11598  ovshftex  11599  shftdm  11602  shftfib  11603  shftval  11605  shftf  11610  crre  11637  cjexp  11673  cjreim2  11685  uzin2  11768  rexuz3  11771  resqrexlemgt0  11801  resqrex  11807  sqrtgt0  11815  sqrtsq  11825  sqrtmsq  11826  absrpclap  11842  absext  11844  absmul  11850  absid  11852  qabscl  11858  absexp  11861  nn0abscl  11867  abslt  11870  absle  11871  recvalap  11879  abstri  11886  caubnd2  11899  qdenre  11984  maxabsle  11986  maxabslemval  11990  maxcl  11992  rexanre  12002  min1inf  12015  minabs  12019  minclpr  12020  mul0inf  12025  mingeb  12026  xrmaxiflemcl  12029  xrnegiso  12046  climconst2  12075  climmpt  12084  climres  12087  climcaucn  12135  sumeq1  12139  summodclem2a  12166  isumz  12174  fisumss  12177  fsumzcl2  12190  sumsnf  12194  isumclim3  12208  fsum2dlemstep  12219  fisumcom2  12223  fsumconst  12239  cvgcmpub  12261  binom  12269  binom1p  12270  binom1dif  12272  bcxmas  12274  divcnv  12282  geo2lim  12301  geoisum  12302  geoisumr  12303  geoisum1  12304  mertenslemi1  12320  mertensabs  12322  prod1dc  12371  fprodconst  12405  fprodcom2fi  12411  efcllem  12444  efcj  12458  efadd  12460  efexp  12467  efgt1p2  12480  tanvalap  12493  tanval2ap  12498  tanval3ap  12499  sinadd  12521  cosadd  12522  dvdsdc  12583  iddvdsexp  12600  dvdsadd  12621  dvds1  12638  odd2np1  12658  oddm1even  12660  m1exp1  12686  divalglemnn  12703  fldivndvdslt  12722  flodddiv4lt  12723  bitsp1  12736  bitsmod  12741  bitsfi  12742  bitscmp  12743  bitsinv1lem  12746  dvdsbnd  12751  gcdnncl  12762  zeqzmulgcd  12765  gcdneg  12777  modgcd  12786  bezoutlemex  12796  bezoutlemeu  12802  dfgcd3  12805  gcdzeq  12817  dvdssq  12826  algrf  12841  eucalgval2  12849  eucalgcvga  12854  lcmval  12859  gcddvdslcm  12869  lcmneg  12870  coprmgcdb  12884  qredeu  12893  divgcdcoprm0  12897  divgcdcoprmex  12898  cncongr1  12899  cncongr2  12900  cncongrcoprm  12902  prmind2  12916  dvdsnprmd  12921  exprmfct  12935  isprm6  12944  pwbdvds  12963  nnmaxpwlemnfac  12969  nnmaxpwlemparts  12970  nnmaxpw  12971  sqrt2irraplemnn  12977  divnumden  12994  divdenle  12995  nn0sqrtelqelz  13004  phivalfi  13012  crth  13024  eulerth  13033  prmdivdiv  13037  reumodprminv  13054  nnnn0modprm0  13056  nnoddn2prmb  13063  pcval  13097  pcidlem  13124  pcid  13125  pcneg  13126  pc2dvds  13131  pcz  13133  pcprod  13147  prmpwdvds  13156  4sqexercise1  13199  2expltfac  13241  prmlem0  13242  ballotfilemfval  13280  ballotfilemefi  13288  ballotfilemodife  13291  ballotfilem4  13292  ballotfilemsval  13303  ballotfilemieq  13311  ballotfilemrv  13314  ballotfilemrinv0  13327  xpct  13338  znnen  13340  ennnfonelemg  13345  ennnfone  13367  ctinfom  13370  ctinf  13372  ssomct  13387  isstruct2im  13413  isstruct2r  13414  setsvalg  13433  setsslnid  13455  ressvalsets  13469  ressex  13470  2strbasg  13525  2stropg  13526  2strbas1g  13528  ressmulrg  13550  ressscag  13588  ressvscag  13589  ressipg  13590  restval  13650  restid2  13653  qusex  13697  fnpr2o  13711  xpsfval  13720  intopsn  13738  mgmidmo  13743  lidrididd  13753  ismnddef  13782  mndinvmod  13809  imasmnd2  13810  ismhm  13819  mhmex  13820  insubm  13843  dfgrp2  13883  grpsubval  13902  grpinvinv  13923  grpsubrcan  13937  grpsubadd  13944  grpaddsubass  13946  grpsubsub4  13949  grppnpcan2  13950  grpnpncan  13951  grpnpncan0  13952  grpnnncan2  13953  dfgrp3m  13955  dfgrp3me  13956  imasgrp2  13964  mhmmnd  13970  mulgfvalg  13975  mulgval  13976  mulgfng  13978  mulg1  13983  mulgnnp1  13984  mulgnndir  14005  mulgass  14013  mulgmodid  14015  issubg2m  14043  grpissubg  14048  isnsg  14056  isnsg3  14061  0nsg  14068  eqgfval  14076  eqger  14078  eqgen  14081  eqgcpbl  14082  quseccl  14087  isghm  14097  kerf1ghm  14128  conjghm  14130  conjsubg  14131  abladdsub  14170  ablpncan3  14172  ablsubsub23  14180  invghm  14184  subgabl  14187  prdsex  14223  xpsval  14252  pwsval  14255  mgpress  14281  rngdi  14290  rnglz  14295  imasrng  14306  srgmulgass  14344  srgrmhm  14349  isring  14355  ringo2times  14384  ringrng  14392  ringlz  14399  imasring  14420  opprrng  14433  opprrngbg  14434  opprring  14435  mulgass3  14442  dvdsrd  14452  dvdsrneg  14461  unitnegcl  14488  dvrvald  14492  dvrid  14495  dvr1  14496  dvrass  14497  dvrdir  14501  ringinvdv  14503  rhmex  14515  isrim0  14519  rhmval  14531  rhmdvdsr  14533  rhmopp  14534  elrhmunit  14535  rhmunitinv  14536  isnzr2  14542  ringelnzr  14545  issubrng2  14569  issubrg2  14600  ringunitap  14644  aprap  14649  aprnzr  14650  opprdrng  14671  lmodvs1  14704  lmod0vs  14709  lmodvs0  14710  lmodvsmmulgdi  14711  lmodfopne  14714  lmodvneg1  14718  lss1  14750  islss3  14767  lsslss  14769  lss1d  14771  lspf  14777  lspsn  14804  lspsnneg  14808  sraval  14825  sraring  14837  qus1  14914  qusrhm  14916  cnfldui  14975  dvdsrzring  14989  mulgghm2  14994  mulgrhm  14995  znval  15022  znf1o  15037  assa2ass  15060  assa2ass2  15061  issubassa3  15063  assamulgscmlem2  15093  psrbagfi  15110  psrbaglefifi  15114  psrbagconcl  15115  psrplusgg  15121  mplgrpfi  15149  eltg2b  15207  difopn  15261  ntrcls0  15284  neii1  15300  restbasg  15321  resttopon  15324  restuni2  15330  cnrest2r  15390  tx1cn  15422  txcnp  15424  txcn  15428  txswaphmeo  15474  psmettri  15483  xmeteq0  15512  xmettri  15525  metrtri  15530  ssblex  15584  xmeter  15589  isxms2  15605  cnbl0  15687  cnblcld  15688  reopnap  15699  tgioo  15707  addcncntoplem  15714  expcn  15722  rescncf  15734  cncfcdm  15735  mulc1cncf  15742  cncfcncntop  15746  addccncf  15753  cdivcncfap  15757  negcncf  15758  cnopnap  15764  suplociccex  15778  hoverlt1  15802  hovergt0  15803  dich0  15805  limccl  15812  ellimc3apf  15813  cnplimcim  15820  limccnp2lem  15829  reldvg  15832  dvbsssg  15839  dvcjbr  15861  dvcj  15862  dvfre  15863  dvrecap  15866  dvef  15880  plyaddcl  15907  plymulcl  15908  plysubcl  15909  plyrecj  15916  reeff1olem  15924  pilem3  15937  ptolemy  15978  rplogcl  16034  rpcxpef  16052  cxprec  16068  rpcxproot  16072  rplogb1  16106  logbgt0b  16124  logbgcd1irr  16125  zprmlogbaplem3  16139  binom4  16141  birthdaylem1g  16147  wilthlem1  16154  sgmnncl  16179  ppiprm  16181  dvdsppwf1o  16205  ppiublem1  16213  ppiqub  16215  chtublem  16217  chtqub  16218  mersenne  16219  lgslem4  16244  lgsval  16245  lgsval2lem  16251  lgsval4a  16263  lgsdir2lem3  16271  lgsdir2  16274  lgsne0  16279  lgsprme0  16283  lgsmulsqcoprm  16287  gausslemma2dlem0a  16290  gausslemma2dlem1a  16299  2lgslem1b  16330  2lgslem2  16333  2lgsoddprm  16354  struct2slots2dom  16401  structvtxval  16402  structiedg0val  16403  struct2griedg  16409  edgstruct  16427  uhgr0vb  16447  incistruhgr  16453  umgrvad2edg  16574  uspgredg2vlem  16583  uspgredg2v  16584  usgredg2v  16587  ushgredgedg  16589  ushgredgedgloop  16591  usgr0vb  16596  uhgr0vusgr  16601  edg0usgr  16610  subupgr  16636  upgrspanop  16646  umgrspanop  16647  usgrspanop  16648  vtxdgfval  16651  wksfval  16685  wlkpropg  16687  uspgr2wlkeq2  16729  uspgr2wlkeqi  16730  upgr2wlkdc  16740  trlsex  16750  clwwlkccatlem  16763  clwwlkng  16768  clwwlkext2edg  16785  clwwlknccat  16786  umgr2cwwkdifex  16788  clwwlknonel  16795  clwwlknonccat  16796  clwwlknonex2lem2  16801  clwwlknun  16804  eupthsg  16808  eupth2lem3lem6fi  16834  dichmul0orlem7  16881  dichmul0or  16882  bj-nnan  16886  bj-indind  17080  bj-omtrans  17104  bj-inf2vnlem1  17118  sscoll2  17136  pw1map  17147  pwtrufal  17149  sssneq  17154  pw1nct  17155  exmidnotnotr  17158  nninfsellemsuc  17177  nninfomnilem  17183  nnnninfex  17187  exmidsbthrlem  17189  qdencn  17194  trilpo  17214  trirec0  17215  apdiff  17219  iswomninnlem  17221  iswomni0  17223  redcwlpo  17227  redc0  17229  reap0  17230  cndcap  17231  dceqnconst  17232  dcapnconst  17233  neapmkv  17240  neap0mkv  17241  als-no-surprise  17269