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  605  pm4.38  607  pm5.21  700  ioran  757  pm3.14  758  pm4.44  784  ordi  821  pm4.39  827  animorl  828  animorlr  830  pm5.16  833  pm5.54dc  923  intnanr  935  intnanrd  937  dcan  939  dedlema  975  dedlemb  976  pm4.42r  977  prlem2  980  ifpdc  985  dfifp2dc  987  simp1l  1045  simp2l  1047  simp3l  1049  3anandis  1381  xordc1  1435  anxordi  1442  falantru  1445  19.26  1527  exsimpl  1663  sbequ2  1815  sbcof2  1856  sbequilem  1884  sbequ8  1893  euan  2134  mooran1  2150  eupickbi  2160  2exeu  2170  dimatis  2195  rexim  2624  r19.26  2657  r19.40  2685  rspcime  2914  rr19.28v  2943  elrab3t  2958  eueq3dc  2977  mosubt  2980  reu6  2992  sbc2iegf  3099  sbcralt  3105  sbcrext  3106  rmob  3122  csbiebt  3164  ssab2  3308  difdif  3329  uneqin  3455  indifdir  3460  undif3ss  3465  rexm  3591  eqifdc  3639  ifandc  3643  ifnebibdc  3648  difsn  3804  opprc1  3878  unissel  3916  ssmin  3941  abssexg  4265  undifexmid  4276  pwntru  4282  exmidundif  4289  exmidundifim  4290  opelopabsb  4347  sess1  4425  ordelord  4469  onin  4474  suctr  4509  abnexg  4534  ifexg  4573  ordtriexmidlem  4608  ordtri2or2exmid  4660  ontri2orexmidim  4661  tfi  4671  peano1  4683  peano2  4684  nnpredcl  4712  0nelxp  4744  0nelelxp  4745  brab2a  4769  mosubopt  4781  posng  4788  opabssxp  4790  ideqg  4870  relssres  5039  trin2  5116  dminss  5139  iota4an  5295  iota2  5304  iotam  5306  fununfun  5360  fun11uni  5387  imadiflem  5396  funimaexg  5401  fneq12  5410  fvelrnb  5674  dffo4  5776  ffnfv  5786  ffvresb  5791  fmptco  5794  fcoconst  5799  funopsn  5810  fcof1  5900  isotr  5933  isopolem  5939  f1oiso  5943  acexmidlemcase  5989  ovprc1  6031  fnoprabg  6096  elovmporab  6196  elovmporab1w  6197  uchoice  6273  op1steq  6315  dmmpog  6345  1stconst  6357  f1o2ndf1  6364  brtpos2  6387  tpostpos  6400  tposf12  6405  smores  6428  tfrlemi1  6468  tfr1onlembfn  6480  tfri1dALT  6487  tfrcllembfn  6493  freceq1  6528  freceq2  6529  frectfr  6536  omv2  6601  omsuc  6608  nnsucelsuc  6627  nntri3  6633  nnaordi  6644  nnmordi  6652  nnm00  6666  ecexr  6675  ertr  6685  swoer  6698  erth  6716  ecelqsdm  6742  iinerm  6744  ecinxp  6747  erovlem  6764  pmresg  6813  resixp  6870  elixpsn  6872  mapsnf1o  6874  dom3  6917  mapdom1g  6996  ssenen  7000  phpelm  7016  finexdc  7052  exmidpweq  7059  nnwetri  7066  fiintim  7081  infidc  7089  ssfii  7129  fiss  7132  dcfi  7136  supubti  7154  supisoex  7164  ordiso2  7190  inl11  7220  omp1eomlem  7249  nnnninf  7281  nninfisol  7288  ctssexmid  7305  ismkvnex  7310  omniwomnimkv  7322  nninfwlpor  7329  nninfwlpoim  7334  nninfinfwlpo  7335  en2eleq  7361  en2other2  7362  exmidfodomrlemr  7368  exmidfodomrlemrALT  7369  acnrcl  7371  exmidaclem  7378  djuen  7381  djudoml  7389  netap  7428  2omotaplemst  7432  exmidapne  7434  cc1  7439  acnccim  7446  dmaddpqlem  7552  distrnqg  7562  ltanqi  7577  ltmnqi  7578  ltaddnq  7582  ltrnqg  7595  ltnnnq  7598  enq0sym  7607  addnq0mo  7622  mulnq0mo  7623  addnnnq0  7624  distrnq0  7634  prarloclemn  7674  prarloc  7678  ltdfpr  7681  genplt2i  7685  addnqprl  7704  addnqpru  7705  nqprl  7726  appdivnq  7738  1idprl  7765  1idpru  7766  ltexpri  7788  recexpr  7813  cauappcvgprlemdisj  7826  archrecpr  7839  addsrmo  7918  mulsrmo  7919  addsrpr  7920  mulsrpr  7921  0idsr  7942  1idsr  7943  archsr  7957  prsradd  7961  prsrlt  7962  caucvgsr  7977  map2psrprg  7980  elrealeu  8004  muladd11r  8290  negeu  8325  pncan  8340  pncan3  8342  negsub  8382  addid0  8507  posdif  8590  ltnegcon1  8598  subge0  8610  suble0  8611  lesub0  8614  reapval  8711  reapneg  8732  ap0gt0  8775  aprcl  8781  lt0ap0  8783  recextlem1  8786  recapb  8806  div0ap  8837  recrecap  8844  rec11ap  8845  recgt0  8985  mulgt1  8998  lerec2  9024  recp1lt1  9034  recreclt  9035  ledivp1  9038  negiso  9090  nnsub  9137  avglt1  9338  nnrecl  9355  nnnn0addcl  9387  elnn0nn  9399  nn0ge2m1nn  9417  zaddcl  9474  eluzadd  9739  infregelbex  9781  divfnzn  9804  qaddcl  9818  qreccl  9825  cnref1o  9834  ge0p1rp  9869  divlt1lt  9908  divle1le  9909  addlelt  9952  xrre3  10006  xltnegi  10019  xaddval  10029  xaddcom  10045  xnegdi  10052  xposdif  10066  ixxssixx  10086  iccshftr  10178  iccshftl  10180  iccdil  10182  icccntr  10184  zltaddlt1le  10191  elfz2  10199  peano2fzr  10221  fzdcel  10224  fzsplit2  10234  fzaddel  10243  fzrev2  10269  fzrev2i  10270  fzrev3  10271  elfz1b  10274  fseq1p1m1  10278  uzsubfz0  10313  fzosubel3  10389  eluzgtdifelfzo  10390  fzofzp1b  10421  elfzomelpfzo  10424  exfzdc  10433  fvinim0ffz  10434  zsupcllemex  10437  infssuzcldc  10442  exbtwnzlemshrink  10455  qbtwnz  10458  qbtwnxr  10464  ico0  10468  elicore  10473  xqltnle  10474  apbtwnz  10481  flqge  10489  flqlt  10490  flqltnz  10494  flqbi2  10498  flqaddz  10504  flqmulnn0  10506  intfracq  10529  flqdiv  10530  q0mod  10564  q1mod  10565  mulp1mod1  10574  q2txmodxeq0  10593  modfzo0difsn  10604  frec2uzuzd  10611  frec2uzltd  10612  frec2uzrand  10614  uzennn  10645  seqfveq2g  10686  seq3split  10697  seqsplitg  10698  seq3caopr  10704  seqcaoprg  10705  seqf1oglem2  10729  seqf1og  10730  exp3vallem  10749  exp3val  10750  expnnval  10751  exp1  10754  expcl2lemap  10760  rpexpcl  10767  expnegzap  10782  mulexp  10787  mulexpzap  10788  leexp2r  10802  leexp1a  10803  sq11  10821  subsq  10855  binom2  10860  binom3  10866  zesq  10867  bernneq  10869  sq11ap  10916  zzlesq  10917  mulsubdivbinom2ap  10920  apexp1  10927  facwordi  10949  facubnd  10954  facavg  10955  bcval  10958  bcval5  10972  hashennn  10989  fihashf1rn  10997  fseq1hash  11010  hashdifsn  11028  hashdifpr  11029  hashxp  11035  fiubz  11038  fiubnn  11039  fnfz0hash  11041  ffzo0hash  11043  hash2en  11052  wrdval  11061  wrdsymb0  11090  ccatsymb  11123  ccatval21sw  11126  lswccatn0lsw  11132  s111  11150  ccat1st1st  11158  lswccats1fst  11161  swrdlen2  11180  swrdfv2  11181  swrdsbslen  11184  swrds1  11186  ccatswrd  11188  pfxval  11192  pfxclg  11196  pfxmpt  11198  pfxid  11204  pfxfv0  11210  pfxtrcfv0  11212  pfxfvlsw  11213  pfxeq  11214  ccatpfx  11219  swrdpfx  11225  lenrevpfxcctswrd  11230  wrdeqs1cat  11238  cats1un  11239  swrdccatin1  11243  pfxccatin12lem2a  11245  pfxccatin12lem1  11246  pfxccatin12lem3  11250  pfxccatin12  11251  swrdccat  11253  pfxccat3a  11256  swrdccat3blem  11257  swrdccat3b  11258  reuccatpfxs1lem  11264  reuccatpfxs1  11265  s2cl  11303  s2fv0g  11305  shftfvalg  11315  ovshftex  11316  shftdm  11319  shftfib  11320  shftval  11322  shftf  11327  crre  11354  cjexp  11390  cjreim2  11401  uzin2  11484  rexuz3  11487  resqrexlemgt0  11517  resqrex  11523  sqrtgt0  11531  sqrtsq  11541  sqrtmsq  11542  absrpclap  11558  absext  11560  absmul  11566  absid  11568  absexp  11576  nn0abscl  11582  abslt  11585  absle  11586  recvalap  11594  abstri  11601  caubnd2  11614  qdenre  11699  maxabsle  11701  maxabslemval  11705  maxcl  11707  rexanre  11717  min1inf  11729  minabs  11733  minclpr  11734  mul0inf  11738  mingeb  11739  xrmaxiflemcl  11742  xrnegiso  11759  climconst2  11788  climmpt  11797  climres  11800  climcaucn  11848  sumeq1  11852  summodclem2a  11878  isumz  11886  fisumss  11889  fsumzcl2  11902  sumsnf  11906  isumclim3  11920  fsum2dlemstep  11931  fisumcom2  11935  fsumconst  11951  cvgcmpub  11973  binom  11981  binom1p  11982  binom1dif  11984  bcxmas  11986  divcnv  11994  geo2lim  12013  geoisum  12014  geoisumr  12015  geoisum1  12016  mertenslemi1  12032  mertensabs  12034  prod1dc  12083  fprodconst  12117  fprodcom2fi  12123  efcllem  12156  efcj  12170  efadd  12172  efexp  12179  efgt1p2  12192  tanvalap  12205  tanval2ap  12210  tanval3ap  12211  sinadd  12233  cosadd  12234  dvdsdc  12295  iddvdsexp  12312  dvdsadd  12333  dvds1  12350  odd2np1  12370  oddm1even  12372  m1exp1  12398  divalglemnn  12415  fldivndvdslt  12434  flodddiv4lt  12435  bitsp1  12448  bitsmod  12453  bitsfi  12454  bitscmp  12455  bitsinv1lem  12458  dvdsbnd  12463  gcdnncl  12474  zeqzmulgcd  12477  gcdneg  12489  modgcd  12498  bezoutlemex  12508  bezoutlemeu  12514  dfgcd3  12517  gcdzeq  12529  dvdssq  12538  algrf  12553  eucalgval2  12561  eucalgcvga  12566  lcmval  12571  gcddvdslcm  12581  lcmneg  12582  coprmgcdb  12596  qredeu  12605  divgcdcoprm0  12609  divgcdcoprmex  12610  cncongr1  12611  cncongr2  12612  cncongrcoprm  12614  prmind2  12628  dvdsnprmd  12633  exprmfct  12646  isprm6  12655  pw2dvdslemn  12673  oddpwdclemdc  12681  sqrt2irraplemnn  12687  divnumden  12704  divdenle  12705  nn0sqrtelqelz  12714  phivalfi  12720  crth  12732  eulerth  12741  prmdivdiv  12745  reumodprminv  12762  nnnn0modprm0  12764  nnoddn2prmb  12771  pcval  12805  pcidlem  12832  pcid  12833  pcneg  12834  pc2dvds  12839  pcz  12841  pcprod  12855  prmpwdvds  12864  4sqexercise1  12907  2expltfac  12948  xpct  12953  znnen  12955  ennnfonelemg  12960  ennnfone  12982  ctinfom  12985  ctinf  12987  ssomct  13002  isstruct2im  13028  isstruct2r  13029  setsvalg  13048  setsslnid  13070  ressvalsets  13083  ressex  13084  2strbasg  13139  2stropg  13140  2strbas1g  13142  ressmulrg  13164  ressscag  13202  ressvscag  13203  ressipg  13204  restval  13264  restid2  13267  prdsex  13288  pwsval  13310  qusex  13344  fnpr2o  13358  xpsfval  13367  xpsval  13371  intopsn  13386  mgmidmo  13391  lidrididd  13401  ismnddef  13437  mndinvmod  13464  imasmnd2  13471  ismhm  13480  mhmex  13481  insubm  13504  dfgrp2  13546  grpsubval  13565  grpinvinv  13586  grpsubrcan  13600  grpsubadd  13607  grpaddsubass  13609  grpsubsub4  13612  grppnpcan2  13613  grpnpncan  13614  grpnpncan0  13615  grpnnncan2  13616  dfgrp3m  13618  dfgrp3me  13619  imasgrp2  13633  mhmmnd  13639  mulgfvalg  13644  mulgval  13645  mulgfng  13647  mulg1  13652  mulgnnp1  13653  mulgnndir  13674  mulgass  13682  mulgmodid  13684  issubg2m  13712  grpissubg  13717  isnsg  13725  isnsg3  13730  0nsg  13737  eqgfval  13745  eqger  13747  eqgen  13750  eqgcpbl  13751  quseccl  13756  isghm  13766  kerf1ghm  13797  conjghm  13799  conjsubg  13800  abladdsub  13838  ablpncan3  13840  ablsubsub23  13848  invghm  13852  subgabl  13855  mgpress  13880  rngdi  13889  rnglz  13894  imasrng  13905  srgmulgass  13938  srgrmhm  13943  isring  13949  ringo2times  13977  ringrng  13985  ringlz  13992  imasring  14013  opprrng  14026  opprrngbg  14027  opprring  14028  mulgass3  14034  dvdsrd  14043  dvdsrneg  14052  unitnegcl  14079  dvrvald  14083  dvrid  14086  dvr1  14087  dvrass  14088  dvrdir  14092  ringinvdv  14094  rhmex  14106  isrim0  14110  rhmval  14122  rhmdvdsr  14124  rhmopp  14125  elrhmunit  14126  rhmunitinv  14127  isnzr2  14133  ringelnzr  14136  issubrng2  14159  issubrg2  14190  aprap  14235  lmodvs1  14265  lmod0vs  14270  lmodvs0  14271  lmodvsmmulgdi  14272  lmodfopne  14275  lmodvneg1  14279  lss1  14311  islss3  14328  lsslss  14330  lss1d  14332  lspf  14338  lspsn  14365  lspsnneg  14369  sraval  14386  sraring  14398  qus1  14475  qusrhm  14477  cnfldui  14538  dvdsrzring  14552  mulgghm2  14557  mulgrhm  14558  znval  14585  znf1o  14600  psrbagfi  14622  psrplusgg  14627  mplgrpfi  14655  eltg2b  14713  difopn  14767  ntrcls0  14790  neii1  14806  restbasg  14827  resttopon  14830  restuni2  14836  cnrest2r  14896  tx1cn  14928  txcnp  14930  txcn  14934  txswaphmeo  14980  psmettri  14989  xmeteq0  15018  xmettri  15031  metrtri  15036  ssblex  15090  xmeter  15095  isxms2  15111  cnbl0  15193  cnblcld  15194  reopnap  15205  tgioo  15213  addcncntoplem  15220  expcn  15228  rescncf  15240  cncfcdm  15241  mulc1cncf  15248  cncfcncntop  15252  addccncf  15259  cdivcncfap  15263  negcncf  15264  cnopnap  15270  suplociccex  15284  hoverlt1  15308  hovergt0  15309  dich0  15311  limccl  15318  ellimc3apf  15319  cnplimcim  15326  limccnp2lem  15335  reldvg  15338  dvbsssg  15345  dvcjbr  15367  dvcj  15368  dvfre  15369  dvrecap  15372  dvef  15386  plyaddcl  15413  plymulcl  15414  plysubcl  15415  plyrecj  15422  reeff1olem  15430  pilem3  15442  ptolemy  15483  rplogcl  15538  rpcxpef  15553  cxprec  15569  rpcxproot  15573  rplogb1  15607  logbgt0b  15625  logbgcd1irr  15626  binom4  15638  wilthlem1  15639  sgmnncl  15647  dvdsppwf1o  15648  mersenne  15656  lgslem4  15667  lgsval  15668  lgsval2lem  15674  lgsval4a  15686  lgsdir2lem3  15694  lgsdir2  15697  lgsne0  15702  lgsprme0  15706  lgsmulsqcoprm  15710  gausslemma2dlem0a  15713  gausslemma2dlem1a  15722  2lgslem1b  15753  2lgslem2  15756  2lgsoddprm  15777  struct2slots2dom  15824  structvtxval  15825  structiedg0val  15826  struct2griedg  15832  edgstruct  15849  uhgr0vb  15869  incistruhgr  15875  umgrvad2edg  15994  uspgredg2vlem  16003  uspgredg2v  16004  usgredg2v  16007  ushgredgedg  16009  ushgredgedgloop  16011  bj-nnan  16030  bj-indind  16225  bj-omtrans  16249  bj-inf2vnlem1  16263  sscoll2  16281  2omap  16290  pw1map  16292  pwtrufal  16294  sssneq  16299  pw1nct  16300  nninfsellemsuc  16309  nninfomnilem  16315  nnnninfex  16319  exmidsbthrlem  16321  qdencn  16326  trilpo  16342  trirec0  16343  apdiff  16347  iswomninnlem  16348  iswomni0  16350  redcwlpo  16354  redc0  16356  reap0  16357  cndcap  16358  dceqnconst  16359  dcapnconst  16360  neapmkv  16367  neap0mkv  16368