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  2055  mooran1  2071  eupickbi  2081  2exeu  2091  dimatis  2116  rexim  2526  r19.26  2558  r19.40  2585  rspcime  2796  rr19.28v  2824  elrab3t  2839  eueq3dc  2858  mosubt  2861  reu6  2873  sbc2iegf  2979  sbcralt  2985  sbcrext  2986  rmob  3001  csbiebt  3039  ssab2  3181  difdif  3201  uneqin  3327  indifdir  3332  undif3ss  3337  rexm  3462  eqifdc  3506  ifandc  3508  difsn  3657  opprc1  3727  unissel  3765  ssmin  3790  abssexg  4106  undifexmid  4117  pwntru  4122  exmidundif  4129  exmidundifim  4130  opelopabsb  4182  sess1  4259  ordelord  4303  onin  4308  suctr  4343  abnexg  4367  ordtriexmidlem  4435  ordtri2or2exmid  4486  tfi  4496  peano1  4508  peano2  4509  nnpredcl  4536  0nelxp  4567  0nelelxp  4568  brab2a  4592  mosubopt  4604  posng  4611  opabssxp  4613  ideqg  4690  relssres  4857  trin2  4930  dminss  4953  iota4an  5107  iota2  5114  fun11uni  5193  imadiflem  5202  funimaexg  5207  fneq12  5216  fvelrnb  5469  dffo4  5568  ffnfv  5578  ffvresb  5583  fmptco  5586  fcoconst  5591  fcof1  5684  isotr  5717  isopolem  5723  f1oiso  5727  acexmidlemcase  5769  ovprc1  5807  fnoprabg  5872  op1steq  6077  dmmpog  6107  1stconst  6118  f1o2ndf1  6125  brtpos2  6148  tpostpos  6161  tposf12  6166  smores  6189  tfrlemi1  6229  tfr1onlembfn  6241  tfri1dALT  6248  tfrcllembfn  6254  freceq1  6289  freceq2  6290  frectfr  6297  omv2  6361  omsuc  6368  nnsucelsuc  6387  nntri3  6393  nnaordi  6404  nnmordi  6412  nnm00  6425  ecexr  6434  ertr  6444  swoer  6457  erth  6473  ecelqsdm  6499  iinerm  6501  ecinxp  6504  erovlem  6521  pmresg  6570  resixp  6627  elixpsn  6629  mapsnf1o  6631  dom3  6670  mapdom1g  6741  ssenen  6745  phpelm  6760  finexdc  6796  nnwetri  6804  fiintim  6817  ssfii  6862  fiss  6865  supubti  6886  supisoex  6896  ordiso2  6920  inl11  6950  omp1eomlem  6979  nnnninf  7023  ctssexmid  7024  ismkvnex  7029  en2eleq  7051  en2other2  7052  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  exmidaclem  7064  djuen  7067  djudoml  7075  dmaddpqlem  7185  distrnqg  7195  ltanqi  7210  ltmnqi  7211  ltaddnq  7215  ltrnqg  7228  ltnnnq  7231  enq0sym  7240  addnq0mo  7255  mulnq0mo  7256  addnnnq0  7257  distrnq0  7267  prarloclemn  7307  prarloc  7311  ltdfpr  7314  genplt2i  7318  addnqprl  7337  addnqpru  7338  nqprl  7359  appdivnq  7371  1idprl  7398  1idpru  7399  ltexpri  7421  recexpr  7446  cauappcvgprlemdisj  7459  archrecpr  7472  addsrmo  7551  mulsrmo  7552  addsrpr  7553  mulsrpr  7554  0idsr  7575  1idsr  7576  archsr  7590  prsradd  7594  prsrlt  7595  caucvgsr  7610  map2psrprg  7613  elrealeu  7637  muladd11r  7918  negeu  7953  pncan  7968  pncan3  7970  negsub  8010  addid0  8135  posdif  8217  ltnegcon1  8225  subge0  8237  suble0  8238  lesub0  8241  reapval  8338  reapneg  8359  ap0gt0  8402  aprcl  8408  lt0ap0  8410  recextlem1  8412  div0ap  8462  recrecap  8469  rec11ap  8470  recgt0  8608  mulgt1  8621  lerec2  8647  recp1lt1  8657  recreclt  8658  ledivp1  8661  negiso  8713  nnsub  8759  avglt1  8958  nnrecl  8975  nnnn0addcl  9007  elnn0nn  9019  nn0ge2m1nn  9037  zaddcl  9094  eluzadd  9354  divfnzn  9413  qaddcl  9427  qreccl  9434  cnref1o  9440  ge0p1rp  9473  divlt1lt  9511  divle1le  9512  addlelt  9555  xrre3  9605  xltnegi  9618  xaddval  9628  xaddcom  9644  xnegdi  9651  xposdif  9665  ixxssixx  9685  iccshftr  9777  iccshftl  9779  iccdil  9781  icccntr  9783  zltaddlt1le  9789  elfz2  9797  peano2fzr  9817  fzdcel  9820  fzsplit2  9830  fzaddel  9839  fzrev2  9865  fzrev2i  9866  fzrev3  9867  elfz1b  9870  fseq1p1m1  9874  uzsubfz0  9906  fzosubel3  9973  eluzgtdifelfzo  9974  fzofzp1b  10005  elfzomelpfzo  10008  exfzdc  10017  fvinim0ffz  10018  exbtwnzlemshrink  10026  qbtwnz  10029  qbtwnxr  10035  ico0  10039  apbtwnz  10047  flqge  10055  flqlt  10056  flqltnz  10060  flqbi2  10064  flqaddz  10070  flqmulnn0  10072  intfracq  10093  flqdiv  10094  q0mod  10128  q1mod  10129  mulp1mod1  10138  q2txmodxeq0  10157  modfzo0difsn  10168  frec2uzuzd  10175  frec2uzltd  10176  frec2uzrand  10178  uzennn  10209  seq3split  10252  seq3caopr  10256  exp3vallem  10294  exp3val  10295  expnnval  10296  exp1  10299  expcl2lemap  10305  rpexpcl  10312  expnegzap  10327  mulexp  10332  mulexpzap  10333  leexp2r  10347  leexp1a  10348  sq11  10365  subsq  10399  binom2  10403  binom3  10409  zesq  10410  bernneq  10412  sq11ap  10458  facwordi  10486  facubnd  10491  facavg  10492  bcval  10495  bcval5  10509  hashennn  10526  fihashf1rn  10535  fseq1hash  10547  hashdifsn  10565  hashdifpr  10566  hashxp  10572  fnfz0hash  10575  ffzo0hash  10577  shftfvalg  10590  ovshftex  10591  shftdm  10594  shftfib  10595  shftval  10597  shftf  10602  crre  10629  cjexp  10665  cjreim2  10676  uzin2  10759  rexuz3  10762  resqrexlemgt0  10792  resqrex  10798  sqrtgt0  10806  sqrtsq  10816  sqrtmsq  10817  absrpclap  10833  absext  10835  absmul  10841  absid  10843  absexp  10851  nn0abscl  10857  abslt  10860  absle  10861  recvalap  10869  abstri  10876  caubnd2  10889  qdenre  10974  maxabsle  10976  maxabslemval  10980  maxcl  10982  rexanre  10992  min1inf  11003  minabs  11007  minclpr  11008  mul0inf  11012  xrmaxiflemcl  11014  xrnegiso  11031  climconst2  11060  climmpt  11069  climres  11072  climcaucn  11120  sumeq1  11124  summodclem2a  11150  isumz  11158  fisumss  11161  fsumzcl2  11174  sumsnf  11178  isumclim3  11192  fsum2dlemstep  11203  fisumcom2  11207  fsumconst  11223  cvgcmpub  11245  binom  11253  binom1p  11254  binom1dif  11256  bcxmas  11258  divcnv  11266  geo2lim  11285  geoisum  11286  geoisumr  11287  geoisum1  11288  mertenslemi1  11304  mertensabs  11306  efcllem  11365  efcj  11379  efadd  11381  efexp  11388  efgt1p2  11401  efler  11405  tanvalap  11415  tanval2ap  11420  tanval3ap  11421  sinadd  11443  cosadd  11444  dvdsdc  11501  iddvdsexp  11517  dvdsadd  11536  dvds1  11551  odd2np1  11570  oddm1even  11572  m1exp1  11598  divalglemnn  11615  fldivndvdslt  11632  flodddiv4lt  11633  zsupcllemex  11639  infssuzcldc  11644  dvdsbnd  11645  gcdnncl  11656  zeqzmulgcd  11659  gcdneg  11670  modgcd  11679  bezoutlemex  11689  bezoutlemeu  11695  dfgcd3  11698  gcdzeq  11710  dvdssq  11719  algrf  11726  eucalgval2  11734  eucalgcvga  11739  lcmval  11744  gcddvdslcm  11754  lcmneg  11755  coprmgcdb  11769  qredeu  11778  divgcdcoprm0  11782  divgcdcoprmex  11783  cncongr1  11784  cncongr2  11785  cncongrcoprm  11787  prmind2  11801  dvdsnprmd  11806  exprmfct  11818  isprm6  11825  pw2dvdslemn  11843  oddpwdclemdc  11851  sqrt2irraplemnn  11857  divnumden  11874  divdenle  11875  nn0sqrtelqelz  11884  phivalfi  11888  crth  11900  xpct  11909  znnen  11911  ennnfonelemg  11916  ennnfone  11938  ctinfom  11941  ctinf  11943  isstruct2im  11969  isstruct2r  11970  setsvalg  11989  setsslnid  12010  ressid2  12018  ressval2  12019  2strbasg  12060  2stropg  12061  2strbas1g  12063  restval  12126  restid2  12129  eltg2b  12223  difopn  12277  ntrcls0  12300  neii1  12316  restbasg  12337  resttopon  12340  restuni2  12346  cnrest2r  12406  tx1cn  12438  txcnp  12440  txcn  12444  txswaphmeo  12490  psmettri  12499  xmeteq0  12528  xmettri  12541  metrtri  12546  ssblex  12600  xmeter  12605  isxms2  12621  cnbl0  12703  cnblcld  12704  reopnap  12707  tgioo  12715  addcncntoplem  12720  rescncf  12737  cncffvrn  12738  mulc1cncf  12745  cncfcncntop  12749  addccncf  12755  cdivcncfap  12756  negcncf  12757  cnopnap  12763  suplociccex  12772  limccl  12797  ellimc3apf  12798  cnplimcim  12805  limccnp2lem  12814  reldvg  12817  dvbsssg  12824  dvcjbr  12841  dvcj  12842  dvfre  12843  dvrecap  12846  dvef  12856  pilem3  12864  ptolemy  12905  bj-nnan  12948  bj-indind  13130  bj-omtrans  13154  bj-inf2vnlem1  13168  sscoll2  13186  pwtrufal  13192  nninfsellemsuc  13208  nninfomnilem  13214  exmidsbthrlem  13217  qdencn  13222  trilpo  13236