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  533  simplrl  535  simprll  537  simprrl  539  anabs1  572  jcab  603  pm4.38  605  pm5.21  696  ioran  753  pm3.14  754  pm4.44  780  ordi  817  pm4.39  823  animorl  824  animorlr  826  pm5.16  829  pm5.54dc  919  intnanr  931  intnanrd  933  dcan  935  dedlema  971  dedlemb  972  pm4.42r  973  prlem2  976  simp1l  1023  simp2l  1025  simp3l  1027  3anandis  1358  xordc1  1404  anxordi  1411  falantru  1414  19.26  1492  exsimpl  1628  sbequ2  1780  sbcof2  1821  sbequilem  1849  sbequ8  1858  euan  2098  mooran1  2114  eupickbi  2124  2exeu  2134  dimatis  2159  rexim  2588  r19.26  2620  r19.40  2648  rspcime  2872  rr19.28v  2901  elrab3t  2916  eueq3dc  2935  mosubt  2938  reu6  2950  sbc2iegf  3057  sbcralt  3063  sbcrext  3064  rmob  3079  csbiebt  3121  ssab2  3264  difdif  3285  uneqin  3411  indifdir  3416  undif3ss  3421  rexm  3547  eqifdc  3593  ifandc  3596  ifnebibdc  3601  difsn  3756  opprc1  3827  unissel  3865  ssmin  3890  abssexg  4212  undifexmid  4223  pwntru  4229  exmidundif  4236  exmidundifim  4237  opelopabsb  4291  sess1  4369  ordelord  4413  onin  4418  suctr  4453  abnexg  4478  ifexg  4517  ordtriexmidlem  4552  ordtri2or2exmid  4604  ontri2orexmidim  4605  tfi  4615  peano1  4627  peano2  4628  nnpredcl  4656  0nelxp  4688  0nelelxp  4689  brab2a  4713  mosubopt  4725  posng  4732  opabssxp  4734  ideqg  4814  relssres  4981  trin2  5058  dminss  5081  iota4an  5236  iota2  5245  iotam  5247  fun11uni  5325  imadiflem  5334  funimaexg  5339  fneq12  5348  fvelrnb  5605  dffo4  5707  ffnfv  5717  ffvresb  5722  fmptco  5725  fcoconst  5730  fcof1  5827  isotr  5860  isopolem  5866  f1oiso  5870  acexmidlemcase  5914  ovprc1  5955  fnoprabg  6020  elovmporab  6120  elovmporab1w  6121  uchoice  6192  op1steq  6234  dmmpog  6264  1stconst  6276  f1o2ndf1  6283  brtpos2  6306  tpostpos  6319  tposf12  6324  smores  6347  tfrlemi1  6387  tfr1onlembfn  6399  tfri1dALT  6406  tfrcllembfn  6412  freceq1  6447  freceq2  6448  frectfr  6455  omv2  6520  omsuc  6527  nnsucelsuc  6546  nntri3  6552  nnaordi  6563  nnmordi  6571  nnm00  6585  ecexr  6594  ertr  6604  swoer  6617  erth  6635  ecelqsdm  6661  iinerm  6663  ecinxp  6666  erovlem  6683  pmresg  6732  resixp  6789  elixpsn  6791  mapsnf1o  6793  dom3  6832  mapdom1g  6905  ssenen  6909  phpelm  6924  finexdc  6960  exmidpweq  6967  nnwetri  6974  fiintim  6987  infidc  6995  ssfii  7035  fiss  7038  dcfi  7042  supubti  7060  supisoex  7070  ordiso2  7096  inl11  7126  omp1eomlem  7155  nnnninf  7187  nninfisol  7194  ctssexmid  7211  ismkvnex  7216  omniwomnimkv  7228  nninfwlpor  7235  nninfwlpoim  7239  en2eleq  7257  en2other2  7258  exmidfodomrlemr  7264  exmidfodomrlemrALT  7265  exmidaclem  7270  djuen  7273  djudoml  7281  netap  7316  2omotaplemst  7320  exmidapne  7322  cc1  7327  dmaddpqlem  7439  distrnqg  7449  ltanqi  7464  ltmnqi  7465  ltaddnq  7469  ltrnqg  7482  ltnnnq  7485  enq0sym  7494  addnq0mo  7509  mulnq0mo  7510  addnnnq0  7511  distrnq0  7521  prarloclemn  7561  prarloc  7565  ltdfpr  7568  genplt2i  7572  addnqprl  7591  addnqpru  7592  nqprl  7613  appdivnq  7625  1idprl  7652  1idpru  7653  ltexpri  7675  recexpr  7700  cauappcvgprlemdisj  7713  archrecpr  7726  addsrmo  7805  mulsrmo  7806  addsrpr  7807  mulsrpr  7808  0idsr  7829  1idsr  7830  archsr  7844  prsradd  7848  prsrlt  7849  caucvgsr  7864  map2psrprg  7867  elrealeu  7891  muladd11r  8177  negeu  8212  pncan  8227  pncan3  8229  negsub  8269  addid0  8394  posdif  8476  ltnegcon1  8484  subge0  8496  suble0  8497  lesub0  8500  reapval  8597  reapneg  8618  ap0gt0  8661  aprcl  8667  lt0ap0  8669  recextlem1  8672  recapb  8692  div0ap  8723  recrecap  8730  rec11ap  8731  recgt0  8871  mulgt1  8884  lerec2  8910  recp1lt1  8920  recreclt  8921  ledivp1  8924  negiso  8976  nnsub  9023  avglt1  9224  nnrecl  9241  nnnn0addcl  9273  elnn0nn  9285  nn0ge2m1nn  9303  zaddcl  9360  eluzadd  9624  infregelbex  9666  divfnzn  9689  qaddcl  9703  qreccl  9710  cnref1o  9719  ge0p1rp  9754  divlt1lt  9793  divle1le  9794  addlelt  9837  xrre3  9891  xltnegi  9904  xaddval  9914  xaddcom  9930  xnegdi  9937  xposdif  9951  ixxssixx  9971  iccshftr  10063  iccshftl  10065  iccdil  10067  icccntr  10069  zltaddlt1le  10076  elfz2  10084  peano2fzr  10106  fzdcel  10109  fzsplit2  10119  fzaddel  10128  fzrev2  10154  fzrev2i  10155  fzrev3  10156  elfz1b  10159  fseq1p1m1  10163  uzsubfz0  10198  fzosubel3  10266  eluzgtdifelfzo  10267  fzofzp1b  10298  elfzomelpfzo  10301  exfzdc  10310  fvinim0ffz  10311  exbtwnzlemshrink  10320  qbtwnz  10323  qbtwnxr  10329  ico0  10333  elicore  10338  xqltnle  10339  apbtwnz  10346  flqge  10354  flqlt  10355  flqltnz  10359  flqbi2  10363  flqaddz  10369  flqmulnn0  10371  intfracq  10394  flqdiv  10395  q0mod  10429  q1mod  10430  mulp1mod1  10439  q2txmodxeq0  10458  modfzo0difsn  10469  frec2uzuzd  10476  frec2uzltd  10477  frec2uzrand  10479  uzennn  10510  seqfveq2g  10551  seq3split  10562  seqsplitg  10563  seq3caopr  10569  seqcaoprg  10570  seqf1oglem2  10594  seqf1og  10595  exp3vallem  10614  exp3val  10615  expnnval  10616  exp1  10619  expcl2lemap  10625  rpexpcl  10632  expnegzap  10647  mulexp  10652  mulexpzap  10653  leexp2r  10667  leexp1a  10668  sq11  10686  subsq  10720  binom2  10725  binom3  10731  zesq  10732  bernneq  10734  sq11ap  10781  zzlesq  10782  mulsubdivbinom2ap  10785  apexp1  10792  facwordi  10814  facubnd  10819  facavg  10820  bcval  10823  bcval5  10837  hashennn  10854  fihashf1rn  10862  fseq1hash  10875  hashdifsn  10893  hashdifpr  10894  hashxp  10900  fiubz  10903  fiubnn  10904  fnfz0hash  10906  ffzo0hash  10908  wrdval  10920  wrdsymb0  10949  shftfvalg  10965  ovshftex  10966  shftdm  10969  shftfib  10970  shftval  10972  shftf  10977  crre  11004  cjexp  11040  cjreim2  11051  uzin2  11134  rexuz3  11137  resqrexlemgt0  11167  resqrex  11173  sqrtgt0  11181  sqrtsq  11191  sqrtmsq  11192  absrpclap  11208  absext  11210  absmul  11216  absid  11218  absexp  11226  nn0abscl  11232  abslt  11235  absle  11236  recvalap  11244  abstri  11251  caubnd2  11264  qdenre  11349  maxabsle  11351  maxabslemval  11355  maxcl  11357  rexanre  11367  min1inf  11378  minabs  11382  minclpr  11383  mul0inf  11387  mingeb  11388  xrmaxiflemcl  11391  xrnegiso  11408  climconst2  11437  climmpt  11446  climres  11449  climcaucn  11497  sumeq1  11501  summodclem2a  11527  isumz  11535  fisumss  11538  fsumzcl2  11551  sumsnf  11555  isumclim3  11569  fsum2dlemstep  11580  fisumcom2  11584  fsumconst  11600  cvgcmpub  11622  binom  11630  binom1p  11631  binom1dif  11633  bcxmas  11635  divcnv  11643  geo2lim  11662  geoisum  11663  geoisumr  11664  geoisum1  11665  mertenslemi1  11681  mertensabs  11683  prod1dc  11732  fprodconst  11766  fprodcom2fi  11772  efcllem  11805  efcj  11819  efadd  11821  efexp  11828  efgt1p2  11841  tanvalap  11854  tanval2ap  11859  tanval3ap  11860  sinadd  11882  cosadd  11883  dvdsdc  11944  iddvdsexp  11961  dvdsadd  11982  dvds1  11998  odd2np1  12017  oddm1even  12019  m1exp1  12045  divalglemnn  12062  fldivndvdslt  12079  flodddiv4lt  12080  zsupcllemex  12086  infssuzcldc  12091  dvdsbnd  12096  gcdnncl  12107  zeqzmulgcd  12110  gcdneg  12122  modgcd  12131  bezoutlemex  12141  bezoutlemeu  12147  dfgcd3  12150  gcdzeq  12162  dvdssq  12171  algrf  12186  eucalgval2  12194  eucalgcvga  12199  lcmval  12204  gcddvdslcm  12214  lcmneg  12215  coprmgcdb  12229  qredeu  12238  divgcdcoprm0  12242  divgcdcoprmex  12243  cncongr1  12244  cncongr2  12245  cncongrcoprm  12247  prmind2  12261  dvdsnprmd  12266  exprmfct  12279  isprm6  12288  pw2dvdslemn  12306  oddpwdclemdc  12314  sqrt2irraplemnn  12320  divnumden  12337  divdenle  12338  nn0sqrtelqelz  12347  phivalfi  12353  crth  12365  eulerth  12374  prmdivdiv  12378  reumodprminv  12394  nnnn0modprm0  12396  nnoddn2prmb  12403  pcval  12437  pcidlem  12464  pcid  12465  pcneg  12466  pc2dvds  12471  pcz  12473  pcprod  12487  prmpwdvds  12496  4sqexercise1  12539  xpct  12556  znnen  12558  ennnfonelemg  12563  ennnfone  12585  ctinfom  12588  ctinf  12590  ssomct  12605  isstruct2im  12631  isstruct2r  12632  setsvalg  12651  setsslnid  12673  ressvalsets  12685  ressex  12686  2strbasg  12740  2stropg  12741  2strbas1g  12743  ressmulrg  12765  ressscag  12803  ressvscag  12804  ressipg  12805  restval  12859  restid2  12862  prdsex  12883  qusex  12911  fnpr2o  12925  xpsfval  12934  xpsval  12938  intopsn  12953  mgmidmo  12958  lidrididd  12968  ismnddef  13002  mndinvmod  13029  ismhm  13036  mhmex  13037  insubm  13060  dfgrp2  13102  grpsubval  13121  grpinvinv  13142  grpsubrcan  13156  grpsubadd  13163  grpaddsubass  13165  grpsubsub4  13168  grppnpcan2  13169  grpnpncan  13170  grpnpncan0  13171  grpnnncan2  13172  dfgrp3m  13174  dfgrp3me  13175  imasgrp2  13183  mhmmnd  13189  mulgfvalg  13194  mulgval  13195  mulgfng  13197  mulg1  13202  mulgnnp1  13203  mulgnndir  13224  mulgass  13232  mulgmodid  13234  issubg2m  13262  grpissubg  13267  isnsg  13275  isnsg3  13280  0nsg  13287  eqgfval  13295  eqger  13297  eqgen  13300  eqgcpbl  13301  quseccl  13306  isghm  13316  kerf1ghm  13347  conjghm  13349  conjsubg  13350  abladdsub  13388  ablpncan3  13390  ablsubsub23  13398  invghm  13402  subgabl  13405  mgpress  13430  rngdi  13439  rnglz  13444  imasrng  13455  srgmulgass  13488  srgrmhm  13493  isring  13499  ringo2times  13527  ringrng  13535  ringlz  13542  imasring  13563  opprrng  13576  opprrngbg  13577  opprring  13578  mulgass3  13584  dvdsrd  13593  dvdsrneg  13602  unitnegcl  13629  dvrvald  13633  dvrid  13636  dvr1  13637  dvrass  13638  dvrdir  13642  ringinvdv  13644  rhmex  13656  isrim0  13660  rhmval  13672  rhmdvdsr  13674  rhmopp  13675  elrhmunit  13676  rhmunitinv  13677  isnzr2  13683  ringelnzr  13686  issubrng2  13709  issubrg2  13740  aprap  13785  lmodvs1  13815  lmod0vs  13820  lmodvs0  13821  lmodvsmmulgdi  13822  lmodfopne  13825  lmodvneg1  13829  lss1  13861  islss3  13878  lsslss  13880  lss1d  13882  lspf  13888  lspsn  13915  lspsnneg  13919  sraval  13936  sraring  13948  qus1  14025  qusrhm  14027  cnfldui  14088  dvdsrzring  14102  mulgghm2  14107  mulgrhm  14108  znval  14135  znf1o  14150  psrplusgg  14173  eltg2b  14233  difopn  14287  ntrcls0  14310  neii1  14326  restbasg  14347  resttopon  14350  restuni2  14356  cnrest2r  14416  tx1cn  14448  txcnp  14450  txcn  14454  txswaphmeo  14500  psmettri  14509  xmeteq0  14538  xmettri  14551  metrtri  14556  ssblex  14610  xmeter  14615  isxms2  14631  cnbl0  14713  cnblcld  14714  reopnap  14725  tgioo  14733  addcncntoplem  14740  expcn  14748  rescncf  14760  cncfcdm  14761  mulc1cncf  14768  cncfcncntop  14772  addccncf  14779  cdivcncfap  14783  negcncf  14784  cnopnap  14790  suplociccex  14804  hoverlt1  14828  hovergt0  14829  dich0  14831  limccl  14838  ellimc3apf  14839  cnplimcim  14846  limccnp2lem  14855  reldvg  14858  dvbsssg  14865  dvcjbr  14887  dvcj  14888  dvfre  14889  dvrecap  14892  dvef  14906  plyaddcl  14933  plymulcl  14934  plysubcl  14935  plyrecj  14941  reeff1olem  14947  pilem3  14959  ptolemy  15000  rplogcl  15055  rpcxpef  15070  cxprec  15086  rpcxproot  15089  rplogb1  15121  logbgt0b  15139  logbgcd1irr  15140  binom4  15152  wilthlem1  15153  lgslem4  15160  lgsval  15161  lgsval2lem  15167  lgsval4a  15179  lgsdir2lem3  15187  lgsdir2  15190  lgsne0  15195  lgsprme0  15199  lgsmulsqcoprm  15203  gausslemma2dlem0a  15206  gausslemma2dlem1a  15215  2lgslem1b  15246  2lgslem2  15249  2lgsoddprm  15270  bj-nnan  15298  bj-indind  15494  bj-omtrans  15518  bj-inf2vnlem1  15532  sscoll2  15550  pwtrufal  15558  sssneq  15562  pw1nct  15563  nninfsellemsuc  15572  nninfomnilem  15578  exmidsbthrlem  15582  qdencn  15587  trilpo  15603  trirec0  15604  apdiff  15608  iswomninnlem  15609  iswomni0  15611  redcwlpo  15615  redc0  15617  reap0  15618  cndcap  15619  dceqnconst  15620  dcapnconst  15621  neapmkv  15628  neap0mkv  15629