Theorem simpl 108

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 105	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-ia1 105

This theorem is referenced by:  simpli  110  simpld  111  imp  123  adantrd  277  iba  298  pm3.41  329  pm4.45im  332  anim12  341  pm4.71  386  adantlr  468  adantrr  470  adantllr  472  adantlrr  474  adantrlr  476  adantrrr  478  simplll  522  simplrl  524  simprll  526  simprrl  528  anabs1  561  jcab  592  pm4.38  594  pm5.21  684  ioran  741  pm3.14  742  pm4.44  768  ordi  805  pm4.39  811  pm5.16  813  pm5.54dc  903  intnanr  915  intnanrd  917  dcan  918  dedlema  953  dedlemb  954  pm4.42r  955  prlem2  958  simp1l  1005  simp2l  1007  simp3l  1009  3anandis  1325  xordc1  1371  anxordi  1378  falantru  1381  19.26  1457  exsimpl  1596  sbequ2  1742  sbcof2  1782  sbequilem  1810  sbequ8  1819  euan  2053  mooran1  2069  eupickbi  2079  2exeu  2089  dimatis  2114  rexim  2524  r19.26  2556  r19.40  2583  rspcime  2791  rr19.28v  2819  elrab3t  2834  eueq3dc  2853  mosubt  2856  reu6  2868  sbc2iegf  2974  sbcralt  2980  sbcrext  2981  rmob  2996  csbiebt  3034  ssab2  3176  difdif  3196  uneqin  3322  indifdir  3327  undif3ss  3332  rexm  3457  eqifdc  3501  ifandc  3503  difsn  3652  opprc1  3722  unissel  3760  ssmin  3785  abssexg  4101  undifexmid  4112  pwntru  4117  exmidundif  4124  exmidundifim  4125  opelopabsb  4177  sess1  4254  ordelord  4298  onin  4303  suctr  4338  abnexg  4362  ordtriexmidlem  4430  ordtri2or2exmid  4481  tfi  4491  peano1  4503  peano2  4504  nnpredcl  4531  0nelxp  4562  0nelelxp  4563  brab2a  4587  mosubopt  4599  posng  4606  opabssxp  4608  ideqg  4685  relssres  4852  trin2  4925  dminss  4948  iota4an  5102  iota2  5109  fun11uni  5188  imadiflem  5197  funimaexg  5202  fneq12  5211  fvelrnb  5462  dffo4  5561  ffnfv  5571  ffvresb  5576  fmptco  5579  fcoconst  5584  fcof1  5677  isotr  5710  isopolem  5716  f1oiso  5720  acexmidlemcase  5762  ovprc1  5800  fnoprabg  5865  op1steq  6070  dmmpog  6100  1stconst  6111  f1o2ndf1  6118  brtpos2  6141  tpostpos  6154  tposf12  6159  smores  6182  tfrlemi1  6222  tfr1onlembfn  6234  tfri1dALT  6241  tfrcllembfn  6247  freceq1  6282  freceq2  6283  frectfr  6290  omv2  6354  omsuc  6361  nnsucelsuc  6380  nntri3  6386  nnaordi  6397  nnmordi  6405  nnm00  6418  ecexr  6427  ertr  6437  swoer  6450  erth  6466  ecelqsdm  6492  iinerm  6494  ecinxp  6497  erovlem  6514  pmresg  6563  resixp  6620  elixpsn  6622  mapsnf1o  6624  dom3  6663  mapdom1g  6734  ssenen  6738  phpelm  6753  finexdc  6789  nnwetri  6797  fiintim  6810  ssfii  6855  fiss  6858  supubti  6879  supisoex  6889  ordiso2  6913  inl11  6943  omp1eomlem  6972  nnnninf  7016  ctssexmid  7017  ismkvnex  7022  en2eleq  7044  en2other2  7045  exmidfodomrlemr  7051  exmidfodomrlemrALT  7052  exmidaclem  7057  djuen  7060  djudoml  7068  dmaddpqlem  7178  distrnqg  7188  ltanqi  7203  ltmnqi  7204  ltaddnq  7208  ltrnqg  7221  ltnnnq  7224  enq0sym  7233  addnq0mo  7248  mulnq0mo  7249  addnnnq0  7250  distrnq0  7260  prarloclemn  7300  prarloc  7304  ltdfpr  7307  genplt2i  7311  addnqprl  7330  addnqpru  7331  nqprl  7352  appdivnq  7364  1idprl  7391  1idpru  7392  ltexpri  7414  recexpr  7439  cauappcvgprlemdisj  7452  archrecpr  7465  addsrmo  7544  mulsrmo  7545  addsrpr  7546  mulsrpr  7547  0idsr  7568  1idsr  7569  archsr  7583  prsradd  7587  prsrlt  7588  caucvgsr  7603  map2psrprg  7606  elrealeu  7630  muladd11r  7911  negeu  7946  pncan  7961  pncan3  7963  negsub  8003  addid0  8128  posdif  8210  ltnegcon1  8218  subge0  8230  suble0  8231  lesub0  8234  reapval  8331  reapneg  8352  ap0gt0  8395  aprcl  8401  lt0ap0  8403  recextlem1  8405  div0ap  8455  recrecap  8462  rec11ap  8463  recgt0  8601  mulgt1  8614  lerec2  8640  recp1lt1  8650  recreclt  8651  ledivp1  8654  negiso  8706  nnsub  8752  avglt1  8951  nnrecl  8968  nnnn0addcl  9000  elnn0nn  9012  nn0ge2m1nn  9030  zaddcl  9087  eluzadd  9347  divfnzn  9406  qaddcl  9420  qreccl  9427  cnref1o  9433  ge0p1rp  9466  divlt1lt  9504  divle1le  9505  addlelt  9548  xrre3  9598  xltnegi  9611  xaddval  9621  xaddcom  9637  xnegdi  9644  xposdif  9658  ixxssixx  9678  iccshftr  9770  iccshftl  9772  iccdil  9774  icccntr  9776  zltaddlt1le  9782  elfz2  9790  peano2fzr  9810  fzdcel  9813  fzsplit2  9823  fzaddel  9832  fzrev2  9858  fzrev2i  9859  fzrev3  9860  elfz1b  9863  fseq1p1m1  9867  uzsubfz0  9899  fzosubel3  9966  eluzgtdifelfzo  9967  fzofzp1b  9998  elfzomelpfzo  10001  exfzdc  10010  fvinim0ffz  10011  exbtwnzlemshrink  10019  qbtwnz  10022  qbtwnxr  10028  ico0  10032  apbtwnz  10040  flqge  10048  flqlt  10049  flqltnz  10053  flqbi2  10057  flqaddz  10063  flqmulnn0  10065  intfracq  10086  flqdiv  10087  q0mod  10121  q1mod  10122  mulp1mod1  10131  q2txmodxeq0  10150  modfzo0difsn  10161  frec2uzuzd  10168  frec2uzltd  10169  frec2uzrand  10171  uzennn  10202  seq3split  10245  seq3caopr  10249  exp3vallem  10287  exp3val  10288  expnnval  10289  exp1  10292  expcl2lemap  10298  rpexpcl  10305  expnegzap  10320  mulexp  10325  mulexpzap  10326  leexp2r  10340  leexp1a  10341  sq11  10358  subsq  10392  binom2  10396  binom3  10402  zesq  10403  bernneq  10405  sq11ap  10451  facwordi  10479  facubnd  10484  facavg  10485  bcval  10488  bcval5  10502  hashennn  10519  fihashf1rn  10528  fseq1hash  10540  hashdifsn  10558  hashdifpr  10559  hashxp  10565  fnfz0hash  10568  ffzo0hash  10570  shftfvalg  10583  ovshftex  10584  shftdm  10587  shftfib  10588  shftval  10590  shftf  10595  crre  10622  cjexp  10658  cjreim2  10669  uzin2  10752  rexuz3  10755  resqrexlemgt0  10785  resqrex  10791  sqrtgt0  10799  sqrtsq  10809  sqrtmsq  10810  absrpclap  10826  absext  10828  absmul  10834  absid  10836  absexp  10844  nn0abscl  10850  abslt  10853  absle  10854  recvalap  10862  abstri  10869  caubnd2  10882  qdenre  10967  maxabsle  10969  maxabslemval  10973  maxcl  10975  rexanre  10985  min1inf  10996  minabs  11000  minclpr  11001  mul0inf  11005  xrmaxiflemcl  11007  xrnegiso  11024  climconst2  11053  climmpt  11062  climres  11065  climcaucn  11113  sumeq1  11117  summodclem2a  11143  isumz  11151  fisumss  11154  fsumzcl2  11167  sumsnf  11171  isumclim3  11185  fsum2dlemstep  11196  fisumcom2  11200  fsumconst  11216  cvgcmpub  11238  binom  11246  binom1p  11247  binom1dif  11249  bcxmas  11251  divcnv  11259  geo2lim  11278  geoisum  11279  geoisumr  11280  geoisum1  11281  mertenslemi1  11297  mertensabs  11299  efcllem  11354  efcj  11368  efadd  11370  efexp  11377  efgt1p2  11390  efler  11394  tanvalap  11404  tanval2ap  11409  tanval3ap  11410  sinadd  11432  cosadd  11433  dvdsdc  11490  iddvdsexp  11506  dvdsadd  11525  dvds1  11540  odd2np1  11559  oddm1even  11561  m1exp1  11587  divalglemnn  11604  fldivndvdslt  11621  flodddiv4lt  11622  zsupcllemex  11628  infssuzcldc  11633  dvdsbnd  11634  gcdnncl  11645  zeqzmulgcd  11648  gcdneg  11659  modgcd  11668  bezoutlemex  11678  bezoutlemeu  11684  dfgcd3  11687  gcdzeq  11699  dvdssq  11708  algrf  11715  eucalgval2  11723  eucalgcvga  11728  lcmval  11733  gcddvdslcm  11743  lcmneg  11744  coprmgcdb  11758  qredeu  11767  divgcdcoprm0  11771  divgcdcoprmex  11772  cncongr1  11773  cncongr2  11774  cncongrcoprm  11776  prmind2  11790  dvdsnprmd  11795  exprmfct  11807  isprm6  11814  pw2dvdslemn  11832  oddpwdclemdc  11840  sqrt2irraplemnn  11846  divnumden  11863  divdenle  11864  nn0sqrtelqelz  11873  phivalfi  11877  crth  11889  xpct  11898  znnen  11900  ennnfonelemg  11905  ennnfone  11927  ctinfom  11930  ctinf  11932  isstruct2im  11958  isstruct2r  11959  setsvalg  11978  setsslnid  11999  ressid2  12007  ressval2  12008  2strbasg  12049  2stropg  12050  2strbas1g  12052  restval  12115  restid2  12118  eltg2b  12212  difopn  12266  ntrcls0  12289  neii1  12305  restbasg  12326  resttopon  12329  restuni2  12335  cnrest2r  12395  tx1cn  12427  txcnp  12429  txcn  12433  txswaphmeo  12479  psmettri  12488  xmeteq0  12517  xmettri  12530  metrtri  12535  ssblex  12589  xmeter  12594  isxms2  12610  cnbl0  12692  cnblcld  12693  reopnap  12696  tgioo  12704  addcncntoplem  12709  rescncf  12726  cncffvrn  12727  mulc1cncf  12734  cncfcncntop  12738  addccncf  12744  cdivcncfap  12745  negcncf  12746  cnopnap  12752  suplociccex  12761  limccl  12786  ellimc3apf  12787  cnplimcim  12794  limccnp2lem  12803  reldvg  12806  dvbsssg  12813  dvcjbr  12830  dvcj  12831  dvfre  12832  dvrecap  12835  dvef  12845  pilem3  12853  ptolemy  12894  bj-nnan  12937  bj-indind  13119  bj-omtrans  13143  bj-inf2vnlem1  13157  sscoll2  13175  pwtrufal  13181  nninfsellemsuc  13197  nninfomnilem  13203  exmidsbthrlem  13206  qdencn  13211  trilpo  13225