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  703  ioran  760  pm3.14  761  pm4.44  787  ordi  824  pm4.39  830  animorl  831  animorlr  833  pm5.16  836  pm5.54dc  926  intnanr  938  intnanrd  940  dcan  942  dedlema  978  dedlemb  979  pm4.42r  980  prlem2  983  ifpdc  988  dfifp2dc  990  simp1l  1048  simp2l  1050  simp3l  1052  3anandis  1384  xordc1  1438  anxordi  1445  falantru  1448  19.26  1530  exsimpl  1666  sbequ2  1817  sbcof2  1858  sbequilem  1886  sbequ8  1895  euan  2136  mooran1  2152  eupickbi  2162  2exeu  2172  dimatis  2197  rexim  2627  r19.26  2660  r19.40  2688  rspcime  2918  rr19.28v  2947  elrab3t  2962  eueq3dc  2981  mosubt  2984  reu6  2996  sbc2iegf  3103  sbcralt  3109  sbcrext  3110  rmob  3126  csbiebt  3168  ssab2  3312  difdif  3334  uneqin  3460  indifdir  3465  undif3ss  3470  rexm  3596  eqifdc  3646  ifandc  3650  ifnebibdc  3655  difsn  3815  opprc1  3889  unissel  3927  ssmin  3952  abssexg  4278  undifexmid  4289  pwntru  4295  exmidundif  4302  exmidundifim  4303  opelopabsb  4360  elopabran  4384  sess1  4440  ordelord  4484  onin  4489  suctr  4524  abnexg  4549  ifexg  4588  ordtriexmidlem  4623  ordtri2or2exmid  4675  ontri2orexmidim  4676  tfi  4686  peano1  4698  peano2  4699  nnpredcl  4727  0nelxp  4759  0nelelxp  4760  brab2a  4785  mosubopt  4797  posng  4804  opabssxp  4806  ideqg  4887  relssres  5057  trin2  5135  dminss  5158  iota4an  5314  iota2  5323  iotam  5325  fununfun  5380  fun11uni  5407  imadiflem  5416  funimaexg  5421  fneq12  5430  fvelrnb  5702  dffo4  5803  ffnfv  5813  ffvresb  5818  fmptco  5821  fcoconst  5826  funopsn  5838  fndmexb  5885  fcof1  5934  isotr  5967  isopolem  5973  f1oiso  5977  acexmidlemcase  6023  ovprc1  6065  fnoprabg  6132  elovmporab  6232  elovmporab1w  6233  uchoice  6309  op1steq  6351  dmmpog  6383  1stconst  6395  f1o2ndf1  6402  suppfnss  6435  suppssfvg  6441  brtpos2  6460  tpostpos  6473  tposf12  6478  smores  6501  tfrlemi1  6541  tfr1onlembfn  6553  tfri1dALT  6560  tfrcllembfn  6566  freceq1  6601  freceq2  6602  frectfr  6609  omv2  6676  omsuc  6683  nnsucelsuc  6702  nntri3  6708  nnaordi  6719  nnmordi  6727  nnm00  6741  ecexr  6750  ertr  6760  swoer  6773  erth  6791  ecelqsdm  6817  iinerm  6819  ecinxp  6822  erovlem  6839  pmresg  6888  resixp  6945  elixpsn  6947  mapsnf1o  6949  dom3  6992  modom  7037  mapdom1g  7076  ssenen  7080  phpelm  7096  finexdc  7135  exmidpweq  7144  nnwetri  7151  fiintim  7166  infidc  7176  ssfii  7216  fiss  7219  dcfi  7223  supubti  7241  supisoex  7251  ordiso2  7277  inl11  7307  omp1eomlem  7336  nnnninf  7368  nninfisol  7375  ctssexmid  7392  ismkvnex  7397  omniwomnimkv  7409  nninfwlpor  7416  nninfwlpoim  7421  nninfinfwlpo  7422  en2eleq  7449  en2other2  7450  exmidfodomrlemr  7456  exmidfodomrlemrALT  7457  acnrcl  7459  exmidaclem  7466  djuen  7469  djudoml  7477  netap  7516  2omotaplemst  7520  exmidapne  7522  cc1  7527  acnccim  7534  dmaddpqlem  7640  distrnqg  7650  ltanqi  7665  ltmnqi  7666  ltaddnq  7670  ltrnqg  7683  ltnnnq  7686  enq0sym  7695  addnq0mo  7710  mulnq0mo  7711  addnnnq0  7712  distrnq0  7722  prarloclemn  7762  prarloc  7766  ltdfpr  7769  genplt2i  7773  addnqprl  7792  addnqpru  7793  nqprl  7814  appdivnq  7826  1idprl  7853  1idpru  7854  ltexpri  7876  recexpr  7901  cauappcvgprlemdisj  7914  archrecpr  7927  addsrmo  8006  mulsrmo  8007  addsrpr  8008  mulsrpr  8009  0idsr  8030  1idsr  8031  archsr  8045  prsradd  8049  prsrlt  8050  caucvgsr  8065  map2psrprg  8068  elrealeu  8092  muladd11r  8378  negeu  8413  pncan  8428  pncan3  8430  negsub  8470  addid0  8595  posdif  8678  ltnegcon1  8686  subge0  8698  suble0  8699  lesub0  8702  reapval  8799  reapneg  8820  ap0gt0  8863  aprcl  8869  lt0ap0  8871  recextlem1  8874  recapb  8894  div0ap  8925  recrecap  8932  rec11ap  8933  recgt0  9073  mulgt1  9086  lerec2  9112  recp1lt1  9122  recreclt  9123  ledivp1  9126  negiso  9178  nnsub  9225  avglt1  9426  nnrecl  9443  nnnn0addcl  9475  elnn0nn  9487  nn0ge2m1nn  9505  zaddcl  9562  eluzmn  9805  eluzadd  9828  infregelbex  9875  divfnzn  9898  qaddcl  9912  qreccl  9919  cnref1o  9928  ge0p1rp  9963  divlt1lt  10002  divle1le  10003  addlelt  10046  xrre3  10100  xltnegi  10113  xaddval  10123  xaddcom  10139  xnegdi  10146  xposdif  10160  ixxssixx  10180  iccshftr  10272  iccshftl  10274  iccdil  10276  icccntr  10278  zltaddlt1le  10285  elfz2  10293  peano2fzr  10315  fzdcel  10318  fzsplit2  10328  fzaddel  10337  fzrev2  10363  fzrev2i  10364  fzrev3  10365  elfz1b  10368  fseq1p1m1  10372  uzsubfz0  10407  fzosubel3  10485  eluzgtdifelfzo  10486  fzofzp1b  10517  elfzomelpfzo  10520  exfzdc  10530  fvinim0ffz  10531  zsupcllemex  10534  infssuzcldc  10539  exbtwnzlemshrink  10552  qbtwnz  10555  qbtwnxr  10561  ico0  10565  elicore  10570  xqltnle  10571  apbtwnz  10578  flqge  10586  flqlt  10587  flqltnz  10591  flqbi2  10595  flqaddz  10601  flqmulnn0  10603  intfracq  10626  flqdiv  10627  q0mod  10661  q1mod  10662  mulp1mod1  10671  q2txmodxeq0  10690  modfzo0difsn  10701  frec2uzuzd  10708  frec2uzltd  10709  frec2uzrand  10711  uzennn  10742  seqfveq2g  10783  seq3split  10794  seqsplitg  10795  seq3caopr  10801  seqcaoprg  10802  seqf1oglem2  10826  seqf1og  10827  exp3vallem  10846  exp3val  10847  expnnval  10848  exp1  10851  expcl2lemap  10857  rpexpcl  10864  expnegzap  10879  mulexp  10884  mulexpzap  10885  leexp2r  10899  leexp1a  10900  sq11  10918  subsq  10952  binom2  10957  binom3  10963  zesq  10964  bernneq  10966  sq11ap  11013  zzlesq  11014  mulsubdivbinom2ap  11017  apexp1  11024  facwordi  11046  facubnd  11051  facavg  11052  bcval  11055  bcval5  11069  hashennn  11086  fihashf1rn  11094  fseq1hash  11108  hashdifsn  11127  hashdifpr  11128  hashxp  11134  fiubz  11137  fiubnn  11138  fnfz0hash  11140  ffzo0hash  11142  hash2en  11151  wrdval  11163  ffz0iswrdnn0  11187  wrdsymb0  11193  ccatsymb  11226  ccatval21sw  11229  lswccatn0lsw  11235  ccatalpha  11237  ccatrcl1  11238  s111  11255  ccat1st1st  11265  lswccats1fst  11268  swrdlen2  11290  swrdfv2  11291  swrdsbslen  11294  swrds1  11296  ccatswrd  11298  pfxval  11302  pfxclg  11306  pfxmpt  11308  pfxid  11314  pfxfv0  11320  pfxtrcfv0  11322  pfxfvlsw  11323  pfxeq  11324  ccatpfx  11329  swrdpfx  11335  lenrevpfxcctswrd  11340  wrdeqs1cat  11348  cats1un  11349  swrdccatin1  11353  pfxccatin12lem2a  11355  pfxccatin12lem1  11356  pfxccatin12lem3  11360  pfxccatin12  11361  swrdccat  11363  pfxccat3a  11366  swrdccat3blem  11367  swrdccat3b  11368  reuccatpfxs1lem  11374  reuccatpfxs1  11375  s2cl  11413  s2fv0g  11415  shftfvalg  11439  ovshftex  11440  shftdm  11443  shftfib  11444  shftval  11446  shftf  11451  crre  11478  cjexp  11514  cjreim2  11525  uzin2  11608  rexuz3  11611  resqrexlemgt0  11641  resqrex  11647  sqrtgt0  11655  sqrtsq  11665  sqrtmsq  11666  absrpclap  11682  absext  11684  absmul  11690  absid  11692  absexp  11700  nn0abscl  11706  abslt  11709  absle  11710  recvalap  11718  abstri  11725  caubnd2  11738  qdenre  11823  maxabsle  11825  maxabslemval  11829  maxcl  11831  rexanre  11841  min1inf  11853  minabs  11857  minclpr  11858  mul0inf  11862  mingeb  11863  xrmaxiflemcl  11866  xrnegiso  11883  climconst2  11912  climmpt  11921  climres  11924  climcaucn  11972  sumeq1  11976  summodclem2a  12003  isumz  12011  fisumss  12014  fsumzcl2  12027  sumsnf  12031  isumclim3  12045  fsum2dlemstep  12056  fisumcom2  12060  fsumconst  12076  cvgcmpub  12098  binom  12106  binom1p  12107  binom1dif  12109  bcxmas  12111  divcnv  12119  geo2lim  12138  geoisum  12139  geoisumr  12140  geoisum1  12141  mertenslemi1  12157  mertensabs  12159  prod1dc  12208  fprodconst  12242  fprodcom2fi  12248  efcllem  12281  efcj  12295  efadd  12297  efexp  12304  efgt1p2  12317  tanvalap  12330  tanval2ap  12335  tanval3ap  12336  sinadd  12358  cosadd  12359  dvdsdc  12420  iddvdsexp  12437  dvdsadd  12458  dvds1  12475  odd2np1  12495  oddm1even  12497  m1exp1  12523  divalglemnn  12540  fldivndvdslt  12559  flodddiv4lt  12560  bitsp1  12573  bitsmod  12578  bitsfi  12579  bitscmp  12580  bitsinv1lem  12583  dvdsbnd  12588  gcdnncl  12599  zeqzmulgcd  12602  gcdneg  12614  modgcd  12623  bezoutlemex  12633  bezoutlemeu  12639  dfgcd3  12642  gcdzeq  12654  dvdssq  12663  algrf  12678  eucalgval2  12686  eucalgcvga  12691  lcmval  12696  gcddvdslcm  12706  lcmneg  12707  coprmgcdb  12721  qredeu  12730  divgcdcoprm0  12734  divgcdcoprmex  12735  cncongr1  12736  cncongr2  12737  cncongrcoprm  12739  prmind2  12753  dvdsnprmd  12758  exprmfct  12771  isprm6  12780  pw2dvdslemn  12798  oddpwdclemdc  12806  sqrt2irraplemnn  12812  divnumden  12829  divdenle  12830  nn0sqrtelqelz  12839  phivalfi  12845  crth  12857  eulerth  12866  prmdivdiv  12870  reumodprminv  12887  nnnn0modprm0  12889  nnoddn2prmb  12896  pcval  12930  pcidlem  12957  pcid  12958  pcneg  12959  pc2dvds  12964  pcz  12966  pcprod  12980  prmpwdvds  12989  4sqexercise1  13032  2expltfac  13073  xpct  13078  znnen  13080  ennnfonelemg  13085  ennnfone  13107  ctinfom  13110  ctinf  13112  ssomct  13127  isstruct2im  13153  isstruct2r  13154  setsvalg  13173  setsslnid  13195  ressvalsets  13208  ressex  13209  2strbasg  13264  2stropg  13265  2strbas1g  13267  ressmulrg  13289  ressscag  13327  ressvscag  13328  ressipg  13329  restval  13389  restid2  13392  prdsex  13413  pwsval  13435  qusex  13469  fnpr2o  13483  xpsfval  13492  xpsval  13496  intopsn  13511  mgmidmo  13516  lidrididd  13526  ismnddef  13562  mndinvmod  13589  imasmnd2  13596  ismhm  13605  mhmex  13606  insubm  13629  dfgrp2  13671  grpsubval  13690  grpinvinv  13711  grpsubrcan  13725  grpsubadd  13732  grpaddsubass  13734  grpsubsub4  13737  grppnpcan2  13738  grpnpncan  13739  grpnpncan0  13740  grpnnncan2  13741  dfgrp3m  13743  dfgrp3me  13744  imasgrp2  13758  mhmmnd  13764  mulgfvalg  13769  mulgval  13770  mulgfng  13772  mulg1  13777  mulgnnp1  13778  mulgnndir  13799  mulgass  13807  mulgmodid  13809  issubg2m  13837  grpissubg  13842  isnsg  13850  isnsg3  13855  0nsg  13862  eqgfval  13870  eqger  13872  eqgen  13875  eqgcpbl  13876  quseccl  13881  isghm  13891  kerf1ghm  13922  conjghm  13924  conjsubg  13925  abladdsub  13963  ablpncan3  13965  ablsubsub23  13973  invghm  13977  subgabl  13980  mgpress  14006  rngdi  14015  rnglz  14020  imasrng  14031  srgmulgass  14064  srgrmhm  14069  isring  14075  ringo2times  14103  ringrng  14111  ringlz  14118  imasring  14139  opprrng  14152  opprrngbg  14153  opprring  14154  mulgass3  14160  dvdsrd  14170  dvdsrneg  14179  unitnegcl  14206  dvrvald  14210  dvrid  14213  dvr1  14214  dvrass  14215  dvrdir  14219  ringinvdv  14221  rhmex  14233  isrim0  14237  rhmval  14249  rhmdvdsr  14251  rhmopp  14252  elrhmunit  14253  rhmunitinv  14254  isnzr2  14260  ringelnzr  14263  issubrng2  14286  issubrg2  14317  aprap  14362  lmodvs1  14392  lmod0vs  14397  lmodvs0  14398  lmodvsmmulgdi  14399  lmodfopne  14402  lmodvneg1  14406  lss1  14438  islss3  14455  lsslss  14457  lss1d  14459  lspf  14465  lspsn  14492  lspsnneg  14496  sraval  14513  sraring  14525  qus1  14602  qusrhm  14604  cnfldui  14665  dvdsrzring  14679  mulgghm2  14684  mulgrhm  14685  znval  14712  znf1o  14727  psrbagfi  14750  psrbagconcl  14753  psrplusgg  14759  mplgrpfi  14787  eltg2b  14845  difopn  14899  ntrcls0  14922  neii1  14938  restbasg  14959  resttopon  14962  restuni2  14968  cnrest2r  15028  tx1cn  15060  txcnp  15062  txcn  15066  txswaphmeo  15112  psmettri  15121  xmeteq0  15150  xmettri  15163  metrtri  15168  ssblex  15222  xmeter  15227  isxms2  15243  cnbl0  15325  cnblcld  15326  reopnap  15337  tgioo  15345  addcncntoplem  15352  expcn  15360  rescncf  15372  cncfcdm  15373  mulc1cncf  15380  cncfcncntop  15384  addccncf  15391  cdivcncfap  15395  negcncf  15396  cnopnap  15402  suplociccex  15416  hoverlt1  15440  hovergt0  15441  dich0  15443  limccl  15450  ellimc3apf  15451  cnplimcim  15458  limccnp2lem  15467  reldvg  15470  dvbsssg  15477  dvcjbr  15499  dvcj  15500  dvfre  15501  dvrecap  15504  dvef  15518  plyaddcl  15545  plymulcl  15546  plysubcl  15547  plyrecj  15554  reeff1olem  15562  pilem3  15574  ptolemy  15615  rplogcl  15670  rpcxpef  15685  cxprec  15701  rpcxproot  15705  rplogb1  15739  logbgt0b  15757  logbgcd1irr  15758  binom4  15770  wilthlem1  15774  sgmnncl  15782  dvdsppwf1o  15783  mersenne  15791  lgslem4  15802  lgsval  15803  lgsval2lem  15809  lgsval4a  15821  lgsdir2lem3  15829  lgsdir2  15832  lgsne0  15837  lgsprme0  15841  lgsmulsqcoprm  15845  gausslemma2dlem0a  15848  gausslemma2dlem1a  15857  2lgslem1b  15888  2lgslem2  15891  2lgsoddprm  15912  struct2slots2dom  15959  structvtxval  15960  structiedg0val  15961  struct2griedg  15967  edgstruct  15985  uhgr0vb  16005  incistruhgr  16011  umgrvad2edg  16132  uspgredg2vlem  16141  uspgredg2v  16142  usgredg2v  16145  ushgredgedg  16147  ushgredgedgloop  16149  usgr0vb  16154  uhgr0vusgr  16159  edg0usgr  16168  subupgr  16194  upgrspanop  16204  umgrspanop  16205  usgrspanop  16206  vtxdgfval  16209  wksfval  16243  wlkpropg  16245  uspgr2wlkeq2  16287  uspgr2wlkeqi  16288  upgr2wlkdc  16298  trlsex  16308  clwwlkccatlem  16321  clwwlkng  16326  clwwlkext2edg  16343  clwwlknccat  16344  umgr2cwwkdifex  16346  clwwlknonel  16353  clwwlknonccat  16354  clwwlknonex2lem2  16359  clwwlknun  16362  eupthsg  16366  eupth2lem3lem6fi  16392  bj-nnan  16434  bj-indind  16628  bj-omtrans  16652  bj-inf2vnlem1  16666  sscoll2  16684  2omap  16695  pw1map  16697  pwtrufal  16699  sssneq  16704  pw1nct  16705  exmidnotnotr  16707  nninfsellemsuc  16718  nninfomnilem  16724  nnnninfex  16728  exmidsbthrlem  16730  qdencn  16735  trilpo  16755  trirec0  16756  apdiff  16760  iswomninnlem  16762  iswomni0  16764  redcwlpo  16768  redc0  16770  reap0  16771  cndcap  16772  dceqnconst  16773  dcapnconst  16774  neapmkv  16781  neap0mkv  16782