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  275  iba  296  pm3.41  327  pm4.45im  330  prth  339  pm4.71  384  adantlr  464  adantrr  466  adantllr  468  adantlrr  470  adantrlr  472  adantrrr  474  simplll  503  simplrl  505  simprll  507  simprrl  509  anabs1  542  jcab  573  pm4.38  575  pm5.21  652  ioran  710  pm3.14  711  pm4.44  737  ordi  771  pm4.39  777  pm5.16  779  pm5.54dc  871  intnanr  883  intnanrd  885  dcan  886  dedlema  921  dedlemb  922  pm4.42r  923  prlem2  926  simp1l  973  simp2l  975  simp3l  977  3anandis  1293  xordc1  1339  anxordi  1346  falantru  1349  19.26  1425  exsimpl  1564  sbequ2  1710  sbcof2  1749  sbequilem  1777  sbequ8  1786  euan  2016  mooran1  2032  eupickbi  2042  2exeu  2052  dimatis  2077  rexim  2485  r19.26  2517  r19.40  2543  rr19.28v  2778  elrab3t  2792  eueq3dc  2811  mosubt  2814  reu6  2826  sbc2iegf  2931  sbcralt  2937  sbcrext  2938  rmob  2953  csbiebt  2989  ssab2  3128  difdif  3148  uneqin  3274  indifdir  3279  undif3ss  3284  rexm  3409  eqifdc  3453  ifandc  3455  difsn  3604  opprc1  3674  unissel  3712  ssmin  3737  abssexg  4046  undifexmid  4057  exmidundif  4067  exmidundifim  4068  opelopabsb  4120  sess1  4197  ordelord  4241  onin  4246  suctr  4281  abnexg  4305  ordtriexmidlem  4373  ordtri2or2exmid  4424  tfi  4434  peano1  4446  peano2  4447  nnpredcl  4474  0nelxp  4505  0nelelxp  4506  brab2a  4530  mosubopt  4542  posng  4549  opabssxp  4551  ideqg  4628  relssres  4793  trin2  4866  dminss  4889  iota4an  5043  iota2  5050  fun11uni  5129  imadiflem  5138  funimaexg  5143  fneq12  5152  fvelrnb  5401  dffo4  5500  ffnfv  5510  ffvresb  5515  fmptco  5518  fcoconst  5523  fcof1  5616  isotr  5649  isopolem  5655  f1oiso  5659  acexmidlemcase  5701  ovprc1  5739  fnoprabg  5804  op1steq  6007  dmmpog  6037  1stconst  6048  f1o2ndf1  6055  sprmpt2  6069  brtpos2  6078  tpostpos  6091  tposf12  6096  smores  6119  tfrlemi1  6159  tfr1onlembfn  6171  tfri1dALT  6178  tfrcllembfn  6184  freceq1  6219  freceq2  6220  frectfr  6227  omv2  6291  omsuc  6298  nnsucelsuc  6317  nntri3  6323  nnaordi  6334  nnmordi  6342  nnm00  6355  ecexr  6364  ertr  6374  swoer  6387  erth  6403  ecelqsdm  6429  iinerm  6431  ecinxp  6434  erovlem  6451  pmresg  6500  resixp  6557  elixpsn  6559  mapsnf1o  6561  dom3  6600  mapdom1g  6670  ssenen  6674  phpelm  6689  finexdc  6725  nnwetri  6733  fiintim  6746  supubti  6801  supisoex  6811  ordiso2  6835  inl11  6865  omp1eomlem  6894  nnnninf  6935  ctssexmid  6936  en2eleq  6960  en2other2  6961  exmidfodomrlemr  6967  exmidfodomrlemrALT  6968  djuen  6971  djudoml  6979  dmaddpqlem  7086  distrnqg  7096  ltanqi  7111  ltmnqi  7112  ltaddnq  7116  ltrnqg  7129  ltnnnq  7132  enq0sym  7141  addnq0mo  7156  mulnq0mo  7157  addnnnq0  7158  distrnq0  7168  prarloclemn  7208  prarloc  7212  ltdfpr  7215  genplt2i  7219  addnqprl  7238  addnqpru  7239  nqprl  7260  appdivnq  7272  1idprl  7299  1idpru  7300  ltexpri  7322  recexpr  7347  cauappcvgprlemdisj  7360  archrecpr  7373  addsrmo  7439  mulsrmo  7440  addsrpr  7441  mulsrpr  7442  0idsr  7463  1idsr  7464  archsr  7477  prsradd  7481  prsrlt  7482  caucvgsr  7497  elrealeu  7517  muladd11r  7789  negeu  7824  pncan  7839  pncan3  7841  negsub  7881  addid0  8002  posdif  8084  ltnegcon1  8092  subge0  8104  suble0  8105  lesub0  8108  reapval  8204  reapneg  8225  ap0gt0  8267  recextlem1  8273  div0ap  8323  recrecap  8330  rec11ap  8331  recgt0  8466  mulgt1  8479  lerec2  8505  recp1lt1  8515  recreclt  8516  ledivp1  8519  negiso  8571  nnsub  8617  avglt1  8810  nnrecl  8827  nnnn0addcl  8859  elnn0nn  8871  nn0ge2m1nn  8889  zaddcl  8946  eluzadd  9204  divfnzn  9263  qaddcl  9277  qreccl  9284  cnref1o  9290  ge0p1rp  9322  divlt1lt  9358  divle1le  9359  addlelt  9396  xrre3  9446  xltnegi  9459  xaddval  9469  xaddcom  9485  xnegdi  9492  xposdif  9506  ixxssixx  9526  iccshftr  9618  iccshftl  9620  iccdil  9622  icccntr  9624  zltaddlt1le  9630  elfz2  9638  peano2fzr  9658  fzdcel  9661  fzsplit2  9671  fzaddel  9680  fzrev2  9706  fzrev2i  9707  fzrev3  9708  elfz1b  9711  fseq1p1m1  9715  uzsubfz0  9747  fzosubel3  9814  eluzgtdifelfzo  9815  fzofzp1b  9846  elfzomelpfzo  9849  exfzdc  9858  fvinim0ffz  9859  exbtwnzlemshrink  9867  qbtwnz  9870  qbtwnxr  9876  ico0  9880  apbtwnz  9888  flqge  9896  flqlt  9897  flqltnz  9901  flqbi2  9905  flqaddz  9911  flqmulnn0  9913  intfracq  9934  flqdiv  9935  q0mod  9969  q1mod  9970  mulp1mod1  9979  q2txmodxeq0  9998  modfzo0difsn  10009  frec2uzuzd  10016  frec2uzltd  10017  frec2uzrand  10019  uzennn  10050  seq3split  10093  seq3caopr  10097  exp3vallem  10135  exp3val  10136  expnnval  10137  exp1  10140  expcl2lemap  10146  rpexpcl  10153  expnegzap  10168  mulexp  10173  mulexpzap  10174  leexp2r  10188  leexp1a  10189  sq11  10206  subsq  10240  binom2  10244  binom3  10250  zesq  10251  bernneq  10253  sq11ap  10299  facwordi  10327  facubnd  10332  facavg  10333  bcval  10336  bcval5  10350  hashennn  10367  fihashf1rn  10376  fseq1hash  10388  hashdifsn  10406  hashdifpr  10407  hashxp  10413  fnfz0hash  10416  ffzo0hash  10418  shftfvalg  10431  ovshftex  10432  shftdm  10435  shftfib  10436  shftval  10438  shftf  10443  crre  10470  cjexp  10506  cjreim2  10517  uzin2  10599  rexuz3  10602  resqrexlemgt0  10632  resqrex  10638  sqrtgt0  10646  sqrtsq  10656  sqrtmsq  10657  absrpclap  10673  absext  10675  absmul  10681  absid  10683  absexp  10691  nn0abscl  10697  abslt  10700  absle  10701  recvalap  10709  abstri  10716  caubnd2  10729  qdenre  10814  maxabsle  10816  maxabslemval  10820  maxcl  10822  rexanre  10832  min1inf  10842  minabs  10846  minclpr  10847  mul0inf  10851  xrmaxiflemcl  10853  xrnegiso  10870  climconst2  10899  climmpt  10908  climres  10911  climcaucn  10959  sumeq1  10963  summodclem2a  10989  isumz  10997  fisumss  11000  fsumzcl2  11013  sumsnf  11017  isumclim3  11031  fsum2dlemstep  11042  fisumcom2  11046  fsumconst  11062  cvgcmpub  11084  binom  11092  binom1p  11093  binom1dif  11095  bcxmas  11097  divcnv  11105  geo2lim  11124  geoisum  11125  geoisumr  11126  geoisum1  11127  mertenslemi1  11143  mertensabs  11145  efcllem  11163  efcj  11177  efadd  11179  efexp  11186  efgt1p2  11199  efler  11203  tanvalap  11213  tanval2ap  11218  tanval3ap  11219  sinadd  11241  cosadd  11242  dvdsdc  11296  iddvdsexp  11312  dvdsadd  11331  dvds1  11346  odd2np1  11365  oddm1even  11367  m1exp1  11393  divalglemnn  11410  fldivndvdslt  11427  flodddiv4lt  11428  zsupcllemex  11434  infssuzcldc  11439  dvdsbnd  11440  gcdnncl  11451  zeqzmulgcd  11454  gcdneg  11465  modgcd  11474  bezoutlemex  11482  bezoutlemeu  11488  dfgcd3  11491  gcdzeq  11503  dvdssq  11512  algrf  11519  eucalgval2  11527  eucalgcvga  11532  lcmval  11537  gcddvdslcm  11547  lcmneg  11548  coprmgcdb  11562  qredeu  11571  divgcdcoprm0  11575  divgcdcoprmex  11576  cncongr1  11577  cncongr2  11578  cncongrcoprm  11580  prmind2  11594  dvdsnprmd  11599  exprmfct  11611  isprm6  11618  pw2dvdslemn  11635  oddpwdclemdc  11643  sqrt2irraplemnn  11649  divnumden  11666  divdenle  11667  nn0sqrtelqelz  11676  phivalfi  11680  crth  11692  xpct  11701  znnen  11703  ennnfonelemg  11708  ennnfone  11730  ctinfom  11733  ctinf  11735  isstruct2im  11751  isstruct2r  11752  setsvalg  11771  setsslnid  11792  ressid2  11800  ressval2  11801  2strbasg  11842  2stropg  11843  2strbas1g  11845  restval  11908  restid2  11911  eltg2b  12005  difopn  12059  ntrcls0  12082  neii1  12098  restbasg  12119  resttopon  12122  restuni2  12128  cnrest2r  12187  tx1cn  12219  txcnp  12221  txcn  12225  psmettri  12258  xmeteq0  12287  xmettri  12300  metrtri  12305  ssblex  12359  xmeter  12364  isxms2  12380  cnbl0  12456  cnblcld  12457  tgioo  12465  rescncf  12481  cncffvrn  12482  mulc1cncf  12489  cncfcncntop  12493  addccncf  12498  cdivcncfap  12499  negcncf  12500  limccl  12510  ellimc3ap  12511  cnplimcim  12516  reldvg  12521  dvbsssg  12528  bj-indind  12715  bj-omtrans  12739  bj-inf2vnlem1  12753  sscoll2  12771  pwtrufal  12777  pwntru  12778  nninfsellemsuc  12792  nninfomnilem  12798  exmidsbthrlem  12801  qdencn  12806  trilpo  12820