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  702  ioran  759  pm3.14  760  pm4.44  786  ordi  823  pm4.39  829  animorl  830  animorlr  832  pm5.16  835  pm5.54dc  925  intnanr  937  intnanrd  939  dcan  941  dedlema  977  dedlemb  978  pm4.42r  979  prlem2  982  ifpdc  987  dfifp2dc  989  simp1l  1047  simp2l  1049  simp3l  1051  3anandis  1383  xordc1  1437  anxordi  1444  falantru  1447  19.26  1529  exsimpl  1665  sbequ2  1817  sbcof2  1858  sbequilem  1886  sbequ8  1895  euan  2136  mooran1  2152  eupickbi  2162  2exeu  2172  dimatis  2197  rexim  2626  r19.26  2659  r19.40  2687  rspcime  2917  rr19.28v  2946  elrab3t  2961  eueq3dc  2980  mosubt  2983  reu6  2995  sbc2iegf  3102  sbcralt  3108  sbcrext  3109  rmob  3125  csbiebt  3167  ssab2  3311  difdif  3332  uneqin  3458  indifdir  3463  undif3ss  3468  rexm  3594  eqifdc  3642  ifandc  3646  ifnebibdc  3651  difsn  3810  opprc1  3884  unissel  3922  ssmin  3947  abssexg  4272  undifexmid  4283  pwntru  4289  exmidundif  4296  exmidundifim  4297  opelopabsb  4354  elopabran  4378  sess1  4434  ordelord  4478  onin  4483  suctr  4518  abnexg  4543  ifexg  4582  ordtriexmidlem  4617  ordtri2or2exmid  4669  ontri2orexmidim  4670  tfi  4680  peano1  4692  peano2  4693  nnpredcl  4721  0nelxp  4753  0nelelxp  4754  brab2a  4779  mosubopt  4791  posng  4798  opabssxp  4800  ideqg  4881  relssres  5051  trin2  5128  dminss  5151  iota4an  5307  iota2  5316  iotam  5318  fununfun  5373  fun11uni  5400  imadiflem  5409  funimaexg  5414  fneq12  5423  fvelrnb  5693  dffo4  5795  ffnfv  5805  ffvresb  5810  fmptco  5813  fcoconst  5818  funopsn  5830  fcof1  5924  isotr  5957  isopolem  5963  f1oiso  5967  acexmidlemcase  6013  ovprc1  6055  fnoprabg  6122  elovmporab  6222  elovmporab1w  6223  uchoice  6300  op1steq  6342  dmmpog  6374  1stconst  6386  f1o2ndf1  6393  brtpos2  6417  tpostpos  6430  tposf12  6435  smores  6458  tfrlemi1  6498  tfr1onlembfn  6510  tfri1dALT  6517  tfrcllembfn  6523  freceq1  6558  freceq2  6559  frectfr  6566  omv2  6633  omsuc  6640  nnsucelsuc  6659  nntri3  6665  nnaordi  6676  nnmordi  6684  nnm00  6698  ecexr  6707  ertr  6717  swoer  6730  erth  6748  ecelqsdm  6774  iinerm  6776  ecinxp  6779  erovlem  6796  pmresg  6845  resixp  6902  elixpsn  6904  mapsnf1o  6906  dom3  6949  modom  6994  mapdom1g  7033  ssenen  7037  phpelm  7053  finexdc  7092  exmidpweq  7101  nnwetri  7108  fiintim  7123  infidc  7133  ssfii  7173  fiss  7176  dcfi  7180  supubti  7198  supisoex  7208  ordiso2  7234  inl11  7264  omp1eomlem  7293  nnnninf  7325  nninfisol  7332  ctssexmid  7349  ismkvnex  7354  omniwomnimkv  7366  nninfwlpor  7373  nninfwlpoim  7378  nninfinfwlpo  7379  en2eleq  7406  en2other2  7407  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  acnrcl  7416  exmidaclem  7423  djuen  7426  djudoml  7434  netap  7473  2omotaplemst  7477  exmidapne  7479  cc1  7484  acnccim  7491  dmaddpqlem  7597  distrnqg  7607  ltanqi  7622  ltmnqi  7623  ltaddnq  7627  ltrnqg  7640  ltnnnq  7643  enq0sym  7652  addnq0mo  7667  mulnq0mo  7668  addnnnq0  7669  distrnq0  7679  prarloclemn  7719  prarloc  7723  ltdfpr  7726  genplt2i  7730  addnqprl  7749  addnqpru  7750  nqprl  7771  appdivnq  7783  1idprl  7810  1idpru  7811  ltexpri  7833  recexpr  7858  cauappcvgprlemdisj  7871  archrecpr  7884  addsrmo  7963  mulsrmo  7964  addsrpr  7965  mulsrpr  7966  0idsr  7987  1idsr  7988  archsr  8002  prsradd  8006  prsrlt  8007  caucvgsr  8022  map2psrprg  8025  elrealeu  8049  muladd11r  8335  negeu  8370  pncan  8385  pncan3  8387  negsub  8427  addid0  8552  posdif  8635  ltnegcon1  8643  subge0  8655  suble0  8656  lesub0  8659  reapval  8756  reapneg  8777  ap0gt0  8820  aprcl  8826  lt0ap0  8828  recextlem1  8831  recapb  8851  div0ap  8882  recrecap  8889  rec11ap  8890  recgt0  9030  mulgt1  9043  lerec2  9069  recp1lt1  9079  recreclt  9080  ledivp1  9083  negiso  9135  nnsub  9182  avglt1  9383  nnrecl  9400  nnnn0addcl  9432  elnn0nn  9444  nn0ge2m1nn  9462  zaddcl  9519  eluzmn  9762  eluzadd  9785  infregelbex  9832  divfnzn  9855  qaddcl  9869  qreccl  9876  cnref1o  9885  ge0p1rp  9920  divlt1lt  9959  divle1le  9960  addlelt  10003  xrre3  10057  xltnegi  10070  xaddval  10080  xaddcom  10096  xnegdi  10103  xposdif  10117  ixxssixx  10137  iccshftr  10229  iccshftl  10231  iccdil  10233  icccntr  10235  zltaddlt1le  10242  elfz2  10250  peano2fzr  10272  fzdcel  10275  fzsplit2  10285  fzaddel  10294  fzrev2  10320  fzrev2i  10321  fzrev3  10322  elfz1b  10325  fseq1p1m1  10329  uzsubfz0  10364  fzosubel3  10442  eluzgtdifelfzo  10443  fzofzp1b  10474  elfzomelpfzo  10477  exfzdc  10487  fvinim0ffz  10488  zsupcllemex  10491  infssuzcldc  10496  exbtwnzlemshrink  10509  qbtwnz  10512  qbtwnxr  10518  ico0  10522  elicore  10527  xqltnle  10528  apbtwnz  10535  flqge  10543  flqlt  10544  flqltnz  10548  flqbi2  10552  flqaddz  10558  flqmulnn0  10560  intfracq  10583  flqdiv  10584  q0mod  10618  q1mod  10619  mulp1mod1  10628  q2txmodxeq0  10647  modfzo0difsn  10658  frec2uzuzd  10665  frec2uzltd  10666  frec2uzrand  10668  uzennn  10699  seqfveq2g  10740  seq3split  10751  seqsplitg  10752  seq3caopr  10758  seqcaoprg  10759  seqf1oglem2  10783  seqf1og  10784  exp3vallem  10803  exp3val  10804  expnnval  10805  exp1  10808  expcl2lemap  10814  rpexpcl  10821  expnegzap  10836  mulexp  10841  mulexpzap  10842  leexp2r  10856  leexp1a  10857  sq11  10875  subsq  10909  binom2  10914  binom3  10920  zesq  10921  bernneq  10923  sq11ap  10970  zzlesq  10971  mulsubdivbinom2ap  10974  apexp1  10981  facwordi  11003  facubnd  11008  facavg  11009  bcval  11012  bcval5  11026  hashennn  11043  fihashf1rn  11051  fseq1hash  11065  hashdifsn  11084  hashdifpr  11085  hashxp  11091  fiubz  11094  fiubnn  11095  fnfz0hash  11097  ffzo0hash  11099  hash2en  11108  wrdval  11120  ffz0iswrdnn0  11144  wrdsymb0  11150  ccatsymb  11183  ccatval21sw  11186  lswccatn0lsw  11192  ccatalpha  11194  ccatrcl1  11195  s111  11212  ccat1st1st  11222  lswccats1fst  11225  swrdlen2  11247  swrdfv2  11248  swrdsbslen  11251  swrds1  11253  ccatswrd  11255  pfxval  11259  pfxclg  11263  pfxmpt  11265  pfxid  11271  pfxfv0  11277  pfxtrcfv0  11279  pfxfvlsw  11280  pfxeq  11281  ccatpfx  11286  swrdpfx  11292  lenrevpfxcctswrd  11297  wrdeqs1cat  11305  cats1un  11306  swrdccatin1  11310  pfxccatin12lem2a  11312  pfxccatin12lem1  11313  pfxccatin12lem3  11317  pfxccatin12  11318  swrdccat  11320  pfxccat3a  11323  swrdccat3blem  11324  swrdccat3b  11325  reuccatpfxs1lem  11331  reuccatpfxs1  11332  s2cl  11370  s2fv0g  11372  shftfvalg  11383  ovshftex  11384  shftdm  11387  shftfib  11388  shftval  11390  shftf  11395  crre  11422  cjexp  11458  cjreim2  11469  uzin2  11552  rexuz3  11555  resqrexlemgt0  11585  resqrex  11591  sqrtgt0  11599  sqrtsq  11609  sqrtmsq  11610  absrpclap  11626  absext  11628  absmul  11634  absid  11636  absexp  11644  nn0abscl  11650  abslt  11653  absle  11654  recvalap  11662  abstri  11669  caubnd2  11682  qdenre  11767  maxabsle  11769  maxabslemval  11773  maxcl  11775  rexanre  11785  min1inf  11797  minabs  11801  minclpr  11802  mul0inf  11806  mingeb  11807  xrmaxiflemcl  11810  xrnegiso  11827  climconst2  11856  climmpt  11865  climres  11868  climcaucn  11916  sumeq1  11920  summodclem2a  11947  isumz  11955  fisumss  11958  fsumzcl2  11971  sumsnf  11975  isumclim3  11989  fsum2dlemstep  12000  fisumcom2  12004  fsumconst  12020  cvgcmpub  12042  binom  12050  binom1p  12051  binom1dif  12053  bcxmas  12055  divcnv  12063  geo2lim  12082  geoisum  12083  geoisumr  12084  geoisum1  12085  mertenslemi1  12101  mertensabs  12103  prod1dc  12152  fprodconst  12186  fprodcom2fi  12192  efcllem  12225  efcj  12239  efadd  12241  efexp  12248  efgt1p2  12261  tanvalap  12274  tanval2ap  12279  tanval3ap  12280  sinadd  12302  cosadd  12303  dvdsdc  12364  iddvdsexp  12381  dvdsadd  12402  dvds1  12419  odd2np1  12439  oddm1even  12441  m1exp1  12467  divalglemnn  12484  fldivndvdslt  12503  flodddiv4lt  12504  bitsp1  12517  bitsmod  12522  bitsfi  12523  bitscmp  12524  bitsinv1lem  12527  dvdsbnd  12532  gcdnncl  12543  zeqzmulgcd  12546  gcdneg  12558  modgcd  12567  bezoutlemex  12577  bezoutlemeu  12583  dfgcd3  12586  gcdzeq  12598  dvdssq  12607  algrf  12622  eucalgval2  12630  eucalgcvga  12635  lcmval  12640  gcddvdslcm  12650  lcmneg  12651  coprmgcdb  12665  qredeu  12674  divgcdcoprm0  12678  divgcdcoprmex  12679  cncongr1  12680  cncongr2  12681  cncongrcoprm  12683  prmind2  12697  dvdsnprmd  12702  exprmfct  12715  isprm6  12724  pw2dvdslemn  12742  oddpwdclemdc  12750  sqrt2irraplemnn  12756  divnumden  12773  divdenle  12774  nn0sqrtelqelz  12783  phivalfi  12789  crth  12801  eulerth  12810  prmdivdiv  12814  reumodprminv  12831  nnnn0modprm0  12833  nnoddn2prmb  12840  pcval  12874  pcidlem  12901  pcid  12902  pcneg  12903  pc2dvds  12908  pcz  12910  pcprod  12924  prmpwdvds  12933  4sqexercise1  12976  2expltfac  13017  xpct  13022  znnen  13024  ennnfonelemg  13029  ennnfone  13051  ctinfom  13054  ctinf  13056  ssomct  13071  isstruct2im  13097  isstruct2r  13098  setsvalg  13117  setsslnid  13139  ressvalsets  13152  ressex  13153  2strbasg  13208  2stropg  13209  2strbas1g  13211  ressmulrg  13233  ressscag  13271  ressvscag  13272  ressipg  13273  restval  13333  restid2  13336  prdsex  13357  pwsval  13379  qusex  13413  fnpr2o  13427  xpsfval  13436  xpsval  13440  intopsn  13455  mgmidmo  13460  lidrididd  13470  ismnddef  13506  mndinvmod  13533  imasmnd2  13540  ismhm  13549  mhmex  13550  insubm  13573  dfgrp2  13615  grpsubval  13634  grpinvinv  13655  grpsubrcan  13669  grpsubadd  13676  grpaddsubass  13678  grpsubsub4  13681  grppnpcan2  13682  grpnpncan  13683  grpnpncan0  13684  grpnnncan2  13685  dfgrp3m  13687  dfgrp3me  13688  imasgrp2  13702  mhmmnd  13708  mulgfvalg  13713  mulgval  13714  mulgfng  13716  mulg1  13721  mulgnnp1  13722  mulgnndir  13743  mulgass  13751  mulgmodid  13753  issubg2m  13781  grpissubg  13786  isnsg  13794  isnsg3  13799  0nsg  13806  eqgfval  13814  eqger  13816  eqgen  13819  eqgcpbl  13820  quseccl  13825  isghm  13835  kerf1ghm  13866  conjghm  13868  conjsubg  13869  abladdsub  13907  ablpncan3  13909  ablsubsub23  13917  invghm  13921  subgabl  13924  mgpress  13950  rngdi  13959  rnglz  13964  imasrng  13975  srgmulgass  14008  srgrmhm  14013  isring  14019  ringo2times  14047  ringrng  14055  ringlz  14062  imasring  14083  opprrng  14096  opprrngbg  14097  opprring  14098  mulgass3  14104  dvdsrd  14114  dvdsrneg  14123  unitnegcl  14150  dvrvald  14154  dvrid  14157  dvr1  14158  dvrass  14159  dvrdir  14163  ringinvdv  14165  rhmex  14177  isrim0  14181  rhmval  14193  rhmdvdsr  14195  rhmopp  14196  elrhmunit  14197  rhmunitinv  14198  isnzr2  14204  ringelnzr  14207  issubrng2  14230  issubrg2  14261  aprap  14306  lmodvs1  14336  lmod0vs  14341  lmodvs0  14342  lmodvsmmulgdi  14343  lmodfopne  14346  lmodvneg1  14350  lss1  14382  islss3  14399  lsslss  14401  lss1d  14403  lspf  14409  lspsn  14436  lspsnneg  14440  sraval  14457  sraring  14469  qus1  14546  qusrhm  14548  cnfldui  14609  dvdsrzring  14623  mulgghm2  14628  mulgrhm  14629  znval  14656  znf1o  14671  psrbagfi  14693  psrplusgg  14698  mplgrpfi  14726  eltg2b  14784  difopn  14838  ntrcls0  14861  neii1  14877  restbasg  14898  resttopon  14901  restuni2  14907  cnrest2r  14967  tx1cn  14999  txcnp  15001  txcn  15005  txswaphmeo  15051  psmettri  15060  xmeteq0  15089  xmettri  15102  metrtri  15107  ssblex  15161  xmeter  15166  isxms2  15182  cnbl0  15264  cnblcld  15265  reopnap  15276  tgioo  15284  addcncntoplem  15291  expcn  15299  rescncf  15311  cncfcdm  15312  mulc1cncf  15319  cncfcncntop  15323  addccncf  15330  cdivcncfap  15334  negcncf  15335  cnopnap  15341  suplociccex  15355  hoverlt1  15379  hovergt0  15380  dich0  15382  limccl  15389  ellimc3apf  15390  cnplimcim  15397  limccnp2lem  15406  reldvg  15409  dvbsssg  15416  dvcjbr  15438  dvcj  15439  dvfre  15440  dvrecap  15443  dvef  15457  plyaddcl  15484  plymulcl  15485  plysubcl  15486  plyrecj  15493  reeff1olem  15501  pilem3  15513  ptolemy  15554  rplogcl  15609  rpcxpef  15624  cxprec  15640  rpcxproot  15644  rplogb1  15678  logbgt0b  15696  logbgcd1irr  15697  binom4  15709  wilthlem1  15710  sgmnncl  15718  dvdsppwf1o  15719  mersenne  15727  lgslem4  15738  lgsval  15739  lgsval2lem  15745  lgsval4a  15757  lgsdir2lem3  15765  lgsdir2  15768  lgsne0  15773  lgsprme0  15777  lgsmulsqcoprm  15781  gausslemma2dlem0a  15784  gausslemma2dlem1a  15793  2lgslem1b  15824  2lgslem2  15827  2lgsoddprm  15848  struct2slots2dom  15895  structvtxval  15896  structiedg0val  15897  struct2griedg  15903  edgstruct  15921  uhgr0vb  15941  incistruhgr  15947  umgrvad2edg  16068  uspgredg2vlem  16077  uspgredg2v  16078  usgredg2v  16081  ushgredgedg  16083  ushgredgedgloop  16085  usgr0vb  16090  uhgr0vusgr  16095  edg0usgr  16104  subupgr  16130  upgrspanop  16140  umgrspanop  16141  usgrspanop  16142  vtxdgfval  16145  wksfval  16179  wlkpropg  16181  uspgr2wlkeq2  16223  uspgr2wlkeqi  16224  upgr2wlkdc  16234  trlsex  16244  clwwlkccatlem  16257  clwwlkng  16262  clwwlkext2edg  16279  clwwlknccat  16280  umgr2cwwkdifex  16282  clwwlknonel  16289  clwwlknonccat  16290  clwwlknonex2lem2  16295  clwwlknun  16298  eupthsg  16302  eupth2lem3lem6fi  16328  bj-nnan  16358  bj-indind  16553  bj-omtrans  16577  bj-inf2vnlem1  16591  sscoll2  16609  2omap  16620  pw1map  16622  pwtrufal  16624  sssneq  16629  pw1nct  16630  nninfsellemsuc  16640  nninfomnilem  16646  nnnninfex  16650  exmidsbthrlem  16652  qdencn  16657  trilpo  16673  trirec0  16674  apdiff  16678  iswomninnlem  16679  iswomni0  16681  redcwlpo  16685  redc0  16687  reap0  16688  cndcap  16689  dceqnconst  16690  dcapnconst  16691  neapmkv  16698  neap0mkv  16699