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  7318  supubti  7339  supisoex  7349  ordiso2  7375  inl11  7405  omp1eomlem  7434  nnnninf  7466  nninfisol  7473  ctssexmid  7490  ismkvnex  7495  omniwomnimkv  7507  nninfwlpor  7514  nninfwlpoim  7519  nninfinfwlpo  7520  en2eleq  7547  en2other2  7548  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  acnrcl  7557  exmidaclem  7564  djuen  7567  djudoml  7575  netap  7620  2omotaplemst  7624  exmidapne  7626  cc1  7631  acnccim  7638  dmaddpqlem  7744  distrnqg  7754  ltanqi  7769  ltmnqi  7770  ltaddnq  7774  ltrnqg  7787  ltnnnq  7790  enq0sym  7799  addnq0mo  7814  mulnq0mo  7815  addnnnq0  7816  distrnq0  7826  prarloclemn  7866  prarloc  7870  ltdfpr  7873  genplt2i  7877  addnqprl  7896  addnqpru  7897  nqprl  7918  appdivnq  7930  1idprl  7957  1idpru  7958  ltexpri  7980  recexpr  8005  cauappcvgprlemdisj  8018  archrecpr  8031  addsrmo  8110  mulsrmo  8111  addsrpr  8112  mulsrpr  8113  0idsr  8134  1idsr  8135  archsr  8149  prsradd  8153  prsrlt  8154  caucvgsr  8169  map2psrprg  8172  elrealeu  8196  muladd11r  8482  negeu  8517  pncan  8532  pncan3  8534  negsub  8574  addid0  8699  addeq0  8703  posdif  8783  ltnegcon1  8791  subge0  8803  suble0  8804  lesub0  8807  reapval  8905  reapneg  8926  ap0gt0  8969  aprcl  8975  lt0ap0  8977  recextlem1  8980  recapb  9002  div0ap  9033  recrecap  9040  rec11ap  9041  recgt0  9181  mulgt1  9194  lerec2  9220  recp1lt1  9230  recreclt  9231  ledivp1  9234  negiso  9286  nnsub  9344  avglt1  9546  nnrecl  9563  nnnn0addcl  9595  elnn0nn  9607  fcdmnn0fsuppg  9620  nn0ge2m1nn  9629  zaddcl  9686  eluzmn  9930  eluzadd  9953  infregelbex  10000  divfnzn  10023  qaddcl  10037  qreccl  10044  cnref1o  10053  ge0p1rp  10088  divlt1lt  10127  divle1le  10128  addlelt  10171  xrre3  10226  xltnegi  10239  xaddval  10249  xaddcom  10265  xnegdi  10272  xposdif  10286  ixxssixx  10306  iccshftr  10398  iccshftl  10400  iccdil  10402  icccntr  10404  zltaddlt1le  10412  elfz2  10420  peano2fzr  10443  fzdcel  10446  fzsplit2  10457  fzaddel  10467  fzrev2  10494  fzrev2i  10495  fzrev3  10496  elfz1b  10499  fseq1p1m1  10503  uzsubfz0  10538  fzosubel3  10616  eluzgtdifelfzo  10617  fzofzp1b  10648  elfzomelpfzo  10651  exfzdc  10661  fvinim0ffz  10662  zsupcllemex  10665  infssuzcldc  10670  exbtwnzlemshrink  10685  qbtwnz  10688  qbtwnxr  10694  ico0  10698  elicore  10703  xqltnle  10704  apbtwnz  10711  flqge  10719  flqlt  10720  flqltnz  10724  flqbi2  10728  flqaddz  10734  flqmulnn0  10736  intfracq  10759  flqdiv  10760  q0mod  10794  q1mod  10795  mulp1mod1  10804  q2txmodxeq0  10823  modfzo0difsn  10834  frec2uzuzd  10841  frec2uzltd  10842  frec2uzrand  10844  uzennn  10875  seqfveq2g  10916  seq3split  10927  seqsplitg  10928  seq3caopr  10934  seqcaoprg  10935  seqf1oglem2  10959  seqf1og  10960  exp3vallem  10979  exp3val  10980  expnnval  10981  exp1  10984  expcl2lemap  10990  rpexpcl  10997  expnegzap  11012  mulexp  11017  mulexpzap  11018  leexp2r  11032  leexp1a  11033  sq11  11051  subsq  11085  binom2  11090  binom3  11096  zesq  11098  bernneq  11100  sq11ap  11147  zzlesq  11148  mulsubdivbinom2ap  11151  apexp1  11158  facwordi  11180  facubnd  11185  facavg  11186  bcval  11189  bcval5  11203  hashennn  11221  fihashf1rn  11229  fseq1hash  11243  hashdifsn  11262  hashdifpr  11263  hashxp  11269  hashmap  11270  fiubz  11274  fiubnn  11275  fnfz0hash  11277  ffzo0hash  11279  ssenneg  11282  hashfibclem  11284  hashf1  11289  hash2en  11297  wrdval  11309  ffz0iswrdnn0  11333  wrdsymb0  11339  ccatsymb  11372  ccatval21sw  11375  lswccatn0lsw  11381  ccatalpha  11383  ccatrcl1  11384  s111  11401  ccat1st1st  11411  lswccats1fst  11414  swrdlen2  11436  swrdfv2  11437  swrdsbslen  11440  swrds1  11442  ccatswrd  11444  pfxval  11448  pfxclg  11452  pfxmpt  11454  pfxid  11460  pfxfv0  11466  pfxtrcfv0  11468  pfxfvlsw  11469  pfxeq  11470  ccatpfx  11475  swrdpfx  11481  lenrevpfxcctswrd  11486  wrdeqs1cat  11494  cats1un  11495  swrdccatin1  11499  pfxccatin12lem2a  11501  pfxccatin12lem1  11502  pfxccatin12lem3  11506  pfxccatin12  11507  swrdccat  11509  pfxccat3a  11512  swrdccat3blem  11513  swrdccat3b  11514  reuccatpfxs1lem  11520  reuccatpfxs1  11521  s2cl  11559  s2fv0g  11561  shftfvalg  11585  ovshftex  11586  shftdm  11589  shftfib  11590  shftval  11592  shftf  11597  crre  11624  cjexp  11660  cjreim2  11672  uzin2  11755  rexuz3  11758  resqrexlemgt0  11788  resqrex  11794  sqrtgt0  11802  sqrtsq  11812  sqrtmsq  11813  absrpclap  11829  absext  11831  absmul  11837  absid  11839  absexp  11847  nn0abscl  11853  abslt  11856  absle  11857  recvalap  11865  abstri  11872  caubnd2  11885  qdenre  11970  maxabsle  11972  maxabslemval  11976  maxcl  11978  rexanre  11988  min1inf  12000  minabs  12004  minclpr  12005  mul0inf  12009  mingeb  12010  xrmaxiflemcl  12013  xrnegiso  12030  climconst2  12059  climmpt  12068  climres  12071  climcaucn  12119  sumeq1  12123  summodclem2a  12150  isumz  12158  fisumss  12161  fsumzcl2  12174  sumsnf  12178  isumclim3  12192  fsum2dlemstep  12203  fisumcom2  12207  fsumconst  12223  cvgcmpub  12245  binom  12253  binom1p  12254  binom1dif  12256  bcxmas  12258  divcnv  12266  geo2lim  12285  geoisum  12286  geoisumr  12287  geoisum1  12288  mertenslemi1  12304  mertensabs  12306  prod1dc  12355  fprodconst  12389  fprodcom2fi  12395  efcllem  12428  efcj  12442  efadd  12444  efexp  12451  efgt1p2  12464  tanvalap  12477  tanval2ap  12482  tanval3ap  12483  sinadd  12505  cosadd  12506  dvdsdc  12567  iddvdsexp  12584  dvdsadd  12605  dvds1  12622  odd2np1  12642  oddm1even  12644  m1exp1  12670  divalglemnn  12687  fldivndvdslt  12706  flodddiv4lt  12707  bitsp1  12720  bitsmod  12725  bitsfi  12726  bitscmp  12727  bitsinv1lem  12730  dvdsbnd  12735  gcdnncl  12746  zeqzmulgcd  12749  gcdneg  12761  modgcd  12770  bezoutlemex  12780  bezoutlemeu  12786  dfgcd3  12789  gcdzeq  12801  dvdssq  12810  algrf  12825  eucalgval2  12833  eucalgcvga  12838  lcmval  12843  gcddvdslcm  12853  lcmneg  12854  coprmgcdb  12868  qredeu  12877  divgcdcoprm0  12881  divgcdcoprmex  12882  cncongr1  12883  cncongr2  12884  cncongrcoprm  12886  prmind2  12900  dvdsnprmd  12905  exprmfct  12918  isprm6  12927  pw2dvdslemn  12945  oddpwdclemdc  12953  sqrt2irraplemnn  12959  divnumden  12976  divdenle  12977  nn0sqrtelqelz  12986  phivalfi  12992  crth  13004  eulerth  13013  prmdivdiv  13017  reumodprminv  13034  nnnn0modprm0  13036  nnoddn2prmb  13043  pcval  13077  pcidlem  13104  pcid  13105  pcneg  13106  pc2dvds  13111  pcz  13113  pcprod  13127  prmpwdvds  13136  4sqexercise1  13179  2expltfac  13220  ballotfilemfval  13231  ballotfilemefi  13239  ballotfilemodife  13242  ballotfilem4  13243  ballotfilemsval  13254  ballotfilemieq  13262  ballotfilemrv  13265  ballotfilemrinv0  13278  xpct  13289  znnen  13291  ennnfonelemg  13296  ennnfone  13318  ctinfom  13321  ctinf  13323  ssomct  13338  isstruct2im  13364  isstruct2r  13365  setsvalg  13384  setsslnid  13406  ressvalsets  13420  ressex  13421  2strbasg  13476  2stropg  13477  2strbas1g  13479  ressmulrg  13501  ressscag  13539  ressvscag  13540  ressipg  13541  restval  13601  restid2  13604  qusex  13648  fnpr2o  13662  xpsfval  13671  intopsn  13689  mgmidmo  13694  lidrididd  13704  ismnddef  13733  mndinvmod  13760  imasmnd2  13761  ismhm  13770  mhmex  13771  insubm  13794  dfgrp2  13834  grpsubval  13853  grpinvinv  13874  grpsubrcan  13888  grpsubadd  13895  grpaddsubass  13897  grpsubsub4  13900  grppnpcan2  13901  grpnpncan  13902  grpnpncan0  13903  grpnnncan2  13904  dfgrp3m  13906  dfgrp3me  13907  imasgrp2  13915  mhmmnd  13921  mulgfvalg  13926  mulgval  13927  mulgfng  13929  mulg1  13934  mulgnnp1  13935  mulgnndir  13956  mulgass  13964  mulgmodid  13966  issubg2m  13994  grpissubg  13999  isnsg  14007  isnsg3  14012  0nsg  14019  eqgfval  14027  eqger  14029  eqgen  14032  eqgcpbl  14033  quseccl  14038  isghm  14048  kerf1ghm  14079  conjghm  14081  conjsubg  14082  abladdsub  14121  ablpncan3  14123  ablsubsub23  14131  invghm  14135  subgabl  14138  prdsex  14174  xpsval  14203  pwsval  14206  mgpress  14232  rngdi  14241  rnglz  14246  imasrng  14257  srgmulgass  14295  srgrmhm  14300  isring  14306  ringo2times  14335  ringrng  14343  ringlz  14350  imasring  14371  opprrng  14384  opprrngbg  14385  opprring  14386  mulgass3  14393  dvdsrd  14403  dvdsrneg  14412  unitnegcl  14439  dvrvald  14443  dvrid  14446  dvr1  14447  dvrass  14448  dvrdir  14452  ringinvdv  14454  rhmex  14466  isrim0  14470  rhmval  14482  rhmdvdsr  14484  rhmopp  14485  elrhmunit  14486  rhmunitinv  14487  isnzr2  14493  ringelnzr  14496  issubrng2  14520  issubrg2  14551  ringunitap  14595  aprap  14600  aprnzr  14601  opprdrng  14622  lmodvs1  14655  lmod0vs  14660  lmodvs0  14661  lmodvsmmulgdi  14662  lmodfopne  14665  lmodvneg1  14669  lss1  14701  islss3  14718  lsslss  14720  lss1d  14722  lspf  14728  lspsn  14755  lspsnneg  14759  sraval  14776  sraring  14788  qus1  14865  qusrhm  14867  cnfldui  14926  dvdsrzring  14940  mulgghm2  14945  mulgrhm  14946  znval  14973  znf1o  14988  assa2ass  15011  assa2ass2  15012  issubassa3  15014  assamulgscmlem2  15044  psrbagfi  15061  psrbagconcl  15065  psrplusgg  15071  mplgrpfi  15099  eltg2b  15157  difopn  15211  ntrcls0  15234  neii1  15250  restbasg  15271  resttopon  15274  restuni2  15280  cnrest2r  15340  tx1cn  15372  txcnp  15374  txcn  15378  txswaphmeo  15424  psmettri  15433  xmeteq0  15462  xmettri  15475  metrtri  15480  ssblex  15534  xmeter  15539  isxms2  15555  cnbl0  15637  cnblcld  15638  reopnap  15649  tgioo  15657  addcncntoplem  15664  expcn  15672  rescncf  15684  cncfcdm  15685  mulc1cncf  15692  cncfcncntop  15696  addccncf  15703  cdivcncfap  15707  negcncf  15708  cnopnap  15714  suplociccex  15728  hoverlt1  15752  hovergt0  15753  dich0  15755  limccl  15762  ellimc3apf  15763  cnplimcim  15770  limccnp2lem  15779  reldvg  15782  dvbsssg  15789  dvcjbr  15811  dvcj  15812  dvfre  15813  dvrecap  15816  dvef  15830  plyaddcl  15857  plymulcl  15858  plysubcl  15859  plyrecj  15866  reeff1olem  15874  pilem3  15887  ptolemy  15928  rplogcl  15984  rpcxpef  16002  cxprec  16018  rpcxproot  16022  rplogb1  16056  logbgt0b  16074  logbgcd1irr  16075  binom4  16087  birthdaylem1g  16093  wilthlem1  16100  sgmnncl  16108  dvdsppwf1o  16109  mersenne  16117  lgslem4  16134  lgsval  16135  lgsval2lem  16141  lgsval4a  16153  lgsdir2lem3  16161  lgsdir2  16164  lgsne0  16169  lgsprme0  16173  lgsmulsqcoprm  16177  gausslemma2dlem0a  16180  gausslemma2dlem1a  16189  2lgslem1b  16220  2lgslem2  16223  2lgsoddprm  16244  struct2slots2dom  16291  structvtxval  16292  structiedg0val  16293  struct2griedg  16299  edgstruct  16317  uhgr0vb  16337  incistruhgr  16343  umgrvad2edg  16464  uspgredg2vlem  16473  uspgredg2v  16474  usgredg2v  16477  ushgredgedg  16479  ushgredgedgloop  16481  usgr0vb  16486  uhgr0vusgr  16491  edg0usgr  16500  subupgr  16526  upgrspanop  16536  umgrspanop  16537  usgrspanop  16538  vtxdgfval  16541  wksfval  16575  wlkpropg  16577  uspgr2wlkeq2  16619  uspgr2wlkeqi  16620  upgr2wlkdc  16630  trlsex  16640  clwwlkccatlem  16653  clwwlkng  16658  clwwlkext2edg  16675  clwwlknccat  16676  umgr2cwwkdifex  16678  clwwlknonel  16685  clwwlknonccat  16686  clwwlknonex2lem2  16691  clwwlknun  16694  eupthsg  16698  eupth2lem3lem6fi  16724  dichmul0orlem7  16771  dichmul0or  16772  bj-nnan  16776  bj-indind  16970  bj-omtrans  16994  bj-inf2vnlem1  17008  sscoll2  17026  pw1map  17037  pwtrufal  17039  sssneq  17044  pw1nct  17045  exmidnotnotr  17048  nninfsellemsuc  17067  nninfomnilem  17073  nnnninfex  17077  exmidsbthrlem  17079  qdencn  17084  trilpo  17104  trirec0  17105  apdiff  17109  iswomninnlem  17111  iswomni0  17113  redcwlpo  17117  redc0  17119  reap0  17120  cndcap  17121  dceqnconst  17122  dcapnconst  17123  neapmkv  17130  neap0mkv  17131  als-no-surprise  17159