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  695  ioran  752  pm3.14  753  pm4.44  779  ordi  816  pm4.39  822  animorl  823  animorlr  825  pm5.16  828  pm5.54dc  918  intnanr  930  intnanrd  932  dcan  933  dedlema  969  dedlemb  970  pm4.42r  971  prlem2  974  simp1l  1021  simp2l  1023  simp3l  1025  3anandis  1347  xordc1  1393  anxordi  1400  falantru  1403  19.26  1479  exsimpl  1615  sbequ2  1767  sbcof2  1808  sbequilem  1836  sbequ8  1845  euan  2080  mooran1  2096  eupickbi  2106  2exeu  2116  dimatis  2141  rexim  2569  r19.26  2601  r19.40  2629  rspcime  2846  rr19.28v  2875  elrab3t  2890  eueq3dc  2909  mosubt  2912  reu6  2924  sbc2iegf  3031  sbcralt  3037  sbcrext  3038  rmob  3053  csbiebt  3094  ssab2  3237  difdif  3258  uneqin  3384  indifdir  3389  undif3ss  3394  rexm  3520  eqifdc  3566  ifandc  3569  difsn  3726  opprc1  3796  unissel  3834  ssmin  3859  abssexg  4177  undifexmid  4188  pwntru  4194  exmidundif  4201  exmidundifim  4202  opelopabsb  4254  sess1  4331  ordelord  4375  onin  4380  suctr  4415  abnexg  4440  ordtriexmidlem  4512  ordtri2or2exmid  4564  ontri2orexmidim  4565  tfi  4575  peano1  4587  peano2  4588  nnpredcl  4616  0nelxp  4648  0nelelxp  4649  brab2a  4673  mosubopt  4685  posng  4692  opabssxp  4694  ideqg  4771  relssres  4938  trin2  5012  dminss  5035  iota4an  5189  iota2  5198  iotam  5200  fun11uni  5278  imadiflem  5287  funimaexg  5292  fneq12  5301  fvelrnb  5555  dffo4  5656  ffnfv  5666  ffvresb  5671  fmptco  5674  fcoconst  5679  fcof1  5774  isotr  5807  isopolem  5813  f1oiso  5817  acexmidlemcase  5860  ovprc1  5901  fnoprabg  5966  op1steq  6170  dmmpog  6200  1stconst  6212  f1o2ndf1  6219  brtpos2  6242  tpostpos  6255  tposf12  6260  smores  6283  tfrlemi1  6323  tfr1onlembfn  6335  tfri1dALT  6342  tfrcllembfn  6348  freceq1  6383  freceq2  6384  frectfr  6391  omv2  6456  omsuc  6463  nnsucelsuc  6482  nntri3  6488  nnaordi  6499  nnmordi  6507  nnm00  6521  ecexr  6530  ertr  6540  swoer  6553  erth  6569  ecelqsdm  6595  iinerm  6597  ecinxp  6600  erovlem  6617  pmresg  6666  resixp  6723  elixpsn  6725  mapsnf1o  6727  dom3  6766  mapdom1g  6837  ssenen  6841  phpelm  6856  finexdc  6892  exmidpweq  6899  nnwetri  6905  fiintim  6918  ssfii  6963  fiss  6966  dcfi  6970  supubti  6988  supisoex  6998  ordiso2  7024  inl11  7054  omp1eomlem  7083  nnnninf  7114  nninfisol  7121  ctssexmid  7138  ismkvnex  7143  omniwomnimkv  7155  nninfwlpor  7162  nninfwlpoim  7166  en2eleq  7184  en2other2  7185  exmidfodomrlemr  7191  exmidfodomrlemrALT  7192  exmidaclem  7197  djuen  7200  djudoml  7208  cc1  7239  dmaddpqlem  7351  distrnqg  7361  ltanqi  7376  ltmnqi  7377  ltaddnq  7381  ltrnqg  7394  ltnnnq  7397  enq0sym  7406  addnq0mo  7421  mulnq0mo  7422  addnnnq0  7423  distrnq0  7433  prarloclemn  7473  prarloc  7477  ltdfpr  7480  genplt2i  7484  addnqprl  7503  addnqpru  7504  nqprl  7525  appdivnq  7537  1idprl  7564  1idpru  7565  ltexpri  7587  recexpr  7612  cauappcvgprlemdisj  7625  archrecpr  7638  addsrmo  7717  mulsrmo  7718  addsrpr  7719  mulsrpr  7720  0idsr  7741  1idsr  7742  archsr  7756  prsradd  7760  prsrlt  7761  caucvgsr  7776  map2psrprg  7779  elrealeu  7803  muladd11r  8087  negeu  8122  pncan  8137  pncan3  8139  negsub  8179  addid0  8304  posdif  8386  ltnegcon1  8394  subge0  8406  suble0  8407  lesub0  8410  reapval  8507  reapneg  8528  ap0gt0  8571  aprcl  8577  lt0ap0  8579  recextlem1  8581  div0ap  8631  recrecap  8638  rec11ap  8639  recgt0  8778  mulgt1  8791  lerec2  8817  recp1lt1  8827  recreclt  8828  ledivp1  8831  negiso  8883  nnsub  8929  avglt1  9128  nnrecl  9145  nnnn0addcl  9177  elnn0nn  9189  nn0ge2m1nn  9207  zaddcl  9264  eluzadd  9527  infregelbex  9569  divfnzn  9592  qaddcl  9606  qreccl  9613  cnref1o  9621  ge0p1rp  9654  divlt1lt  9693  divle1le  9694  addlelt  9737  xrre3  9791  xltnegi  9804  xaddval  9814  xaddcom  9830  xnegdi  9837  xposdif  9851  ixxssixx  9871  iccshftr  9963  iccshftl  9965  iccdil  9967  icccntr  9969  zltaddlt1le  9976  elfz2  9984  peano2fzr  10005  fzdcel  10008  fzsplit2  10018  fzaddel  10027  fzrev2  10053  fzrev2i  10054  fzrev3  10055  elfz1b  10058  fseq1p1m1  10062  uzsubfz0  10097  fzosubel3  10164  eluzgtdifelfzo  10165  fzofzp1b  10196  elfzomelpfzo  10199  exfzdc  10208  fvinim0ffz  10209  exbtwnzlemshrink  10217  qbtwnz  10220  qbtwnxr  10226  ico0  10230  elicore  10235  apbtwnz  10242  flqge  10250  flqlt  10251  flqltnz  10255  flqbi2  10259  flqaddz  10265  flqmulnn0  10267  intfracq  10288  flqdiv  10289  q0mod  10323  q1mod  10324  mulp1mod1  10333  q2txmodxeq0  10352  modfzo0difsn  10363  frec2uzuzd  10370  frec2uzltd  10371  frec2uzrand  10373  uzennn  10404  seq3split  10447  seq3caopr  10451  exp3vallem  10489  exp3val  10490  expnnval  10491  exp1  10494  expcl2lemap  10500  rpexpcl  10507  expnegzap  10522  mulexp  10527  mulexpzap  10528  leexp2r  10542  leexp1a  10543  sq11  10560  subsq  10594  binom2  10599  binom3  10605  zesq  10606  bernneq  10608  sq11ap  10655  apexp1  10664  facwordi  10686  facubnd  10691  facavg  10692  bcval  10695  bcval5  10709  hashennn  10726  fihashf1rn  10734  fseq1hash  10747  hashdifsn  10765  hashdifpr  10766  hashxp  10772  fiubz  10775  fiubnn  10776  fnfz0hash  10778  ffzo0hash  10780  shftfvalg  10793  ovshftex  10794  shftdm  10797  shftfib  10798  shftval  10800  shftf  10805  crre  10832  cjexp  10868  cjreim2  10879  uzin2  10962  rexuz3  10965  resqrexlemgt0  10995  resqrex  11001  sqrtgt0  11009  sqrtsq  11019  sqrtmsq  11020  absrpclap  11036  absext  11038  absmul  11044  absid  11046  absexp  11054  nn0abscl  11060  abslt  11063  absle  11064  recvalap  11072  abstri  11079  caubnd2  11092  qdenre  11177  maxabsle  11179  maxabslemval  11183  maxcl  11185  rexanre  11195  min1inf  11206  minabs  11210  minclpr  11211  mul0inf  11215  mingeb  11216  xrmaxiflemcl  11219  xrnegiso  11236  climconst2  11265  climmpt  11274  climres  11277  climcaucn  11325  sumeq1  11329  summodclem2a  11355  isumz  11363  fisumss  11366  fsumzcl2  11379  sumsnf  11383  isumclim3  11397  fsum2dlemstep  11408  fisumcom2  11412  fsumconst  11428  cvgcmpub  11450  binom  11458  binom1p  11459  binom1dif  11461  bcxmas  11463  divcnv  11471  geo2lim  11490  geoisum  11491  geoisumr  11492  geoisum1  11493  mertenslemi1  11509  mertensabs  11511  prod1dc  11560  fprodconst  11594  fprodcom2fi  11600  efcllem  11633  efcj  11647  efadd  11649  efexp  11656  efgt1p2  11669  tanvalap  11682  tanval2ap  11687  tanval3ap  11688  sinadd  11710  cosadd  11711  dvdsdc  11771  iddvdsexp  11788  dvdsadd  11809  dvds1  11824  odd2np1  11843  oddm1even  11845  m1exp1  11871  divalglemnn  11888  fldivndvdslt  11905  flodddiv4lt  11906  zsupcllemex  11912  infssuzcldc  11917  dvdsbnd  11922  gcdnncl  11933  zeqzmulgcd  11936  gcdneg  11948  modgcd  11957  bezoutlemex  11967  bezoutlemeu  11973  dfgcd3  11976  gcdzeq  11988  dvdssq  11997  algrf  12010  eucalgval2  12018  eucalgcvga  12023  lcmval  12028  gcddvdslcm  12038  lcmneg  12039  coprmgcdb  12053  qredeu  12062  divgcdcoprm0  12066  divgcdcoprmex  12067  cncongr1  12068  cncongr2  12069  cncongrcoprm  12071  prmind2  12085  dvdsnprmd  12090  exprmfct  12103  isprm6  12112  pw2dvdslemn  12130  oddpwdclemdc  12138  sqrt2irraplemnn  12144  divnumden  12161  divdenle  12162  nn0sqrtelqelz  12171  phivalfi  12177  crth  12189  eulerth  12198  prmdivdiv  12202  reumodprminv  12218  nnnn0modprm0  12220  nnoddn2prmb  12227  pcval  12261  pcidlem  12287  pcid  12288  pcneg  12289  pc2dvds  12294  pcz  12296  pcprod  12309  prmpwdvds  12318  xpct  12362  znnen  12364  ennnfonelemg  12369  ennnfone  12391  ctinfom  12394  ctinf  12396  ssomct  12411  isstruct2im  12437  isstruct2r  12438  setsvalg  12457  setsslnid  12478  ressid2  12488  ressval2  12489  2strbasg  12530  2stropg  12531  2strbas1g  12533  restval  12614  restid2  12617  intopsn  12650  mgmidmo  12655  lidrididd  12665  ismnddef  12683  mndinvmod  12707  ismhm  12714  insubm  12732  dfgrp2  12762  grpsubval  12779  grpinvinv  12796  grpsubrcan  12810  grpsubadd  12817  grpaddsubass  12819  grpsubsub4  12822  grppnpcan2  12823  grpnpncan  12824  grpnpncan0  12825  grpnnncan2  12826  dfgrp3m  12828  dfgrp3me  12829  mhmmnd  12839  mulgfvalg  12844  mulgval  12845  mulgfng  12846  mulg1  12849  mulgnnp1  12850  mulgnndir  12870  mulgass  12878  mulgmodid  12880  abladdsub  12914  ablpncan3  12916  ablsubsub23  12924  srgmulgass  12965  srgrmhm  12970  isring  12976  rngo2times  13004  ringlz  13014  eltg2b  13105  difopn  13159  ntrcls0  13182  neii1  13198  restbasg  13219  resttopon  13222  restuni2  13228  cnrest2r  13288  tx1cn  13320  txcnp  13322  txcn  13326  txswaphmeo  13372  psmettri  13381  xmeteq0  13410  xmettri  13423  metrtri  13428  ssblex  13482  xmeter  13487  isxms2  13503  cnbl0  13585  cnblcld  13586  reopnap  13589  tgioo  13597  addcncntoplem  13602  rescncf  13619  cncfcdm  13620  mulc1cncf  13627  cncfcncntop  13631  addccncf  13637  cdivcncfap  13638  negcncf  13639  cnopnap  13645  suplociccex  13654  limccl  13679  ellimc3apf  13680  cnplimcim  13687  limccnp2lem  13696  reldvg  13699  dvbsssg  13706  dvcjbr  13723  dvcj  13724  dvfre  13725  dvrecap  13728  dvef  13739  reeff1olem  13743  pilem3  13755  ptolemy  13796  rplogcl  13851  rpcxpef  13866  cxprec  13882  rpcxproot  13885  rplogb1  13917  logbgt0b  13935  logbgcd1irr  13936  binom4  13948  lgslem4  13955  lgsval  13956  lgsval2lem  13962  lgsval4a  13974  lgsdir2lem3  13982  lgsdir2  13985  lgsne0  13990  lgsprme0  13994  lgsmulsqcoprm  13998  bj-nnan  14028  bj-indind  14224  bj-omtrans  14248  bj-inf2vnlem1  14262  sscoll2  14280  pwtrufal  14287  sssneq  14292  pw1nct  14293  nninfsellemsuc  14302  nninfomnilem  14308  exmidsbthrlem  14311  qdencn  14316  trilpo  14332  trirec0  14333  apdiff  14337  iswomninnlem  14338  iswomni0  14340  redcwlpo  14344  redc0  14346  reap0  14347  dceqnconst  14348  dcapnconst  14349  neapmkv  14356