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  342  pm4.71  387  adantlr  469  adantrr  471  adantllr  473  adantlrr  475  adantrlr  477  adantrrr  479  simplll  523  simplrl  525  simprll  527  simprrl  529  anabs1  562  jcab  593  pm4.38  595  pm5.21  685  ioran  742  pm3.14  743  pm4.44  769  ordi  806  pm4.39  812  animorl  813  animorlr  815  pm5.16  818  pm5.54dc  908  intnanr  920  intnanrd  922  dcan  923  dedlema  958  dedlemb  959  pm4.42r  960  prlem2  963  simp1l  1010  simp2l  1012  simp3l  1014  3anandis  1336  xordc1  1382  anxordi  1389  falantru  1392  19.26  1468  exsimpl  1604  sbequ2  1756  sbcof2  1797  sbequilem  1825  sbequ8  1834  euan  2069  mooran1  2085  eupickbi  2095  2exeu  2105  dimatis  2130  rexim  2558  r19.26  2590  r19.40  2618  rspcime  2832  rr19.28v  2861  elrab3t  2876  eueq3dc  2895  mosubt  2898  reu6  2910  sbc2iegf  3016  sbcralt  3022  sbcrext  3023  rmob  3038  csbiebt  3079  ssab2  3221  difdif  3242  uneqin  3368  indifdir  3373  undif3ss  3378  rexm  3503  eqifdc  3549  ifandc  3551  difsn  3704  opprc1  3774  unissel  3812  ssmin  3837  abssexg  4155  undifexmid  4166  pwntru  4172  exmidundif  4179  exmidundifim  4180  opelopabsb  4232  sess1  4309  ordelord  4353  onin  4358  suctr  4393  abnexg  4418  ordtriexmidlem  4490  ordtri2or2exmid  4542  ontri2orexmidim  4543  tfi  4553  peano1  4565  peano2  4566  nnpredcl  4594  0nelxp  4626  0nelelxp  4627  brab2a  4651  mosubopt  4663  posng  4670  opabssxp  4672  ideqg  4749  relssres  4916  trin2  4989  dminss  5012  iota4an  5166  iota2  5173  fun11uni  5252  imadiflem  5261  funimaexg  5266  fneq12  5275  fvelrnb  5528  dffo4  5627  ffnfv  5637  ffvresb  5642  fmptco  5645  fcoconst  5650  fcof1  5745  isotr  5778  isopolem  5784  f1oiso  5788  acexmidlemcase  5831  ovprc1  5869  fnoprabg  5934  op1steq  6139  dmmpog  6169  1stconst  6180  f1o2ndf1  6187  brtpos2  6210  tpostpos  6223  tposf12  6228  smores  6251  tfrlemi1  6291  tfr1onlembfn  6303  tfri1dALT  6310  tfrcllembfn  6316  freceq1  6351  freceq2  6352  frectfr  6359  omv2  6424  omsuc  6431  nnsucelsuc  6450  nntri3  6456  nnaordi  6467  nnmordi  6475  nnm00  6488  ecexr  6497  ertr  6507  swoer  6520  erth  6536  ecelqsdm  6562  iinerm  6564  ecinxp  6567  erovlem  6584  pmresg  6633  resixp  6690  elixpsn  6692  mapsnf1o  6694  dom3  6733  mapdom1g  6804  ssenen  6808  phpelm  6823  finexdc  6859  exmidpweq  6866  nnwetri  6872  fiintim  6885  ssfii  6930  fiss  6933  dcfi  6937  supubti  6955  supisoex  6965  ordiso2  6991  inl11  7021  omp1eomlem  7050  nnnninf  7081  nninfisol  7088  ctssexmid  7105  ismkvnex  7110  omniwomnimkv  7122  en2eleq  7142  en2other2  7143  exmidfodomrlemr  7149  exmidfodomrlemrALT  7150  exmidaclem  7155  djuen  7158  djudoml  7166  cc1  7197  dmaddpqlem  7309  distrnqg  7319  ltanqi  7334  ltmnqi  7335  ltaddnq  7339  ltrnqg  7352  ltnnnq  7355  enq0sym  7364  addnq0mo  7379  mulnq0mo  7380  addnnnq0  7381  distrnq0  7391  prarloclemn  7431  prarloc  7435  ltdfpr  7438  genplt2i  7442  addnqprl  7461  addnqpru  7462  nqprl  7483  appdivnq  7495  1idprl  7522  1idpru  7523  ltexpri  7545  recexpr  7570  cauappcvgprlemdisj  7583  archrecpr  7596  addsrmo  7675  mulsrmo  7676  addsrpr  7677  mulsrpr  7678  0idsr  7699  1idsr  7700  archsr  7714  prsradd  7718  prsrlt  7719  caucvgsr  7734  map2psrprg  7737  elrealeu  7761  muladd11r  8045  negeu  8080  pncan  8095  pncan3  8097  negsub  8137  addid0  8262  posdif  8344  ltnegcon1  8352  subge0  8364  suble0  8365  lesub0  8368  reapval  8465  reapneg  8486  ap0gt0  8529  aprcl  8535  lt0ap0  8537  recextlem1  8539  div0ap  8589  recrecap  8596  rec11ap  8597  recgt0  8736  mulgt1  8749  lerec2  8775  recp1lt1  8785  recreclt  8786  ledivp1  8789  negiso  8841  nnsub  8887  avglt1  9086  nnrecl  9103  nnnn0addcl  9135  elnn0nn  9147  nn0ge2m1nn  9165  zaddcl  9222  eluzadd  9485  infregelbex  9527  divfnzn  9550  qaddcl  9564  qreccl  9571  cnref1o  9579  ge0p1rp  9612  divlt1lt  9651  divle1le  9652  addlelt  9695  xrre3  9749  xltnegi  9762  xaddval  9772  xaddcom  9788  xnegdi  9795  xposdif  9809  ixxssixx  9829  iccshftr  9921  iccshftl  9923  iccdil  9925  icccntr  9927  zltaddlt1le  9934  elfz2  9942  peano2fzr  9962  fzdcel  9965  fzsplit2  9975  fzaddel  9984  fzrev2  10010  fzrev2i  10011  fzrev3  10012  elfz1b  10015  fseq1p1m1  10019  uzsubfz0  10054  fzosubel3  10121  eluzgtdifelfzo  10122  fzofzp1b  10153  elfzomelpfzo  10156  exfzdc  10165  fvinim0ffz  10166  exbtwnzlemshrink  10174  qbtwnz  10177  qbtwnxr  10183  ico0  10187  elicore  10192  apbtwnz  10199  flqge  10207  flqlt  10208  flqltnz  10212  flqbi2  10216  flqaddz  10222  flqmulnn0  10224  intfracq  10245  flqdiv  10246  q0mod  10280  q1mod  10281  mulp1mod1  10290  q2txmodxeq0  10309  modfzo0difsn  10320  frec2uzuzd  10327  frec2uzltd  10328  frec2uzrand  10330  uzennn  10361  seq3split  10404  seq3caopr  10408  exp3vallem  10446  exp3val  10447  expnnval  10448  exp1  10451  expcl2lemap  10457  rpexpcl  10464  expnegzap  10479  mulexp  10484  mulexpzap  10485  leexp2r  10499  leexp1a  10500  sq11  10517  subsq  10551  binom2  10555  binom3  10561  zesq  10562  bernneq  10564  sq11ap  10611  apexp1  10620  facwordi  10642  facubnd  10647  facavg  10648  bcval  10651  bcval5  10665  hashennn  10682  fihashf1rn  10691  fseq1hash  10703  hashdifsn  10721  hashdifpr  10722  hashxp  10728  fnfz0hash  10731  ffzo0hash  10733  shftfvalg  10746  ovshftex  10747  shftdm  10750  shftfib  10751  shftval  10753  shftf  10758  crre  10785  cjexp  10821  cjreim2  10832  uzin2  10915  rexuz3  10918  resqrexlemgt0  10948  resqrex  10954  sqrtgt0  10962  sqrtsq  10972  sqrtmsq  10973  absrpclap  10989  absext  10991  absmul  10997  absid  10999  absexp  11007  nn0abscl  11013  abslt  11016  absle  11017  recvalap  11025  abstri  11032  caubnd2  11045  qdenre  11130  maxabsle  11132  maxabslemval  11136  maxcl  11138  rexanre  11148  min1inf  11159  minabs  11163  minclpr  11164  mul0inf  11168  mingeb  11169  xrmaxiflemcl  11172  xrnegiso  11189  climconst2  11218  climmpt  11227  climres  11230  climcaucn  11278  sumeq1  11282  summodclem2a  11308  isumz  11316  fisumss  11319  fsumzcl2  11332  sumsnf  11336  isumclim3  11350  fsum2dlemstep  11361  fisumcom2  11365  fsumconst  11381  cvgcmpub  11403  binom  11411  binom1p  11412  binom1dif  11414  bcxmas  11416  divcnv  11424  geo2lim  11443  geoisum  11444  geoisumr  11445  geoisum1  11446  mertenslemi1  11462  mertensabs  11464  prod1dc  11513  fprodconst  11547  fprodcom2fi  11553  efcllem  11586  efcj  11600  efadd  11602  efexp  11609  efgt1p2  11622  tanvalap  11635  tanval2ap  11640  tanval3ap  11641  sinadd  11663  cosadd  11664  dvdsdc  11724  iddvdsexp  11741  dvdsadd  11761  dvds1  11776  odd2np1  11795  oddm1even  11797  m1exp1  11823  divalglemnn  11840  fldivndvdslt  11857  flodddiv4lt  11858  zsupcllemex  11864  infssuzcldc  11869  dvdsbnd  11874  gcdnncl  11885  zeqzmulgcd  11888  gcdneg  11900  modgcd  11909  bezoutlemex  11919  bezoutlemeu  11925  dfgcd3  11928  gcdzeq  11940  dvdssq  11949  algrf  11956  eucalgval2  11964  eucalgcvga  11969  lcmval  11974  gcddvdslcm  11984  lcmneg  11985  coprmgcdb  11999  qredeu  12008  divgcdcoprm0  12012  divgcdcoprmex  12013  cncongr1  12014  cncongr2  12015  cncongrcoprm  12017  prmind2  12031  dvdsnprmd  12036  exprmfct  12049  isprm6  12056  pw2dvdslemn  12074  oddpwdclemdc  12082  sqrt2irraplemnn  12088  divnumden  12105  divdenle  12106  nn0sqrtelqelz  12115  phivalfi  12121  crth  12133  eulerth  12142  prmdivdiv  12146  reumodprminv  12162  nnnn0modprm0  12164  nnoddn2prmb  12171  pcval  12205  pcidlem  12231  pcid  12232  pcneg  12233  pc2dvds  12238  pcz  12240  pcprod  12253  xpct  12266  znnen  12268  ennnfonelemg  12273  ennnfone  12295  ctinfom  12298  ctinf  12300  ssomct  12315  isstruct2im  12341  isstruct2r  12342  setsvalg  12361  setsslnid  12382  ressid2  12390  ressval2  12391  2strbasg  12432  2stropg  12433  2strbas1g  12435  restval  12498  restid2  12501  eltg2b  12595  difopn  12649  ntrcls0  12672  neii1  12688  restbasg  12709  resttopon  12712  restuni2  12718  cnrest2r  12778  tx1cn  12810  txcnp  12812  txcn  12816  txswaphmeo  12862  psmettri  12871  xmeteq0  12900  xmettri  12913  metrtri  12918  ssblex  12972  xmeter  12977  isxms2  12993  cnbl0  13075  cnblcld  13076  reopnap  13079  tgioo  13087  addcncntoplem  13092  rescncf  13109  cncffvrn  13110  mulc1cncf  13117  cncfcncntop  13121  addccncf  13127  cdivcncfap  13128  negcncf  13129  cnopnap  13135  suplociccex  13144  limccl  13169  ellimc3apf  13170  cnplimcim  13177  limccnp2lem  13186  reldvg  13189  dvbsssg  13196  dvcjbr  13213  dvcj  13214  dvfre  13215  dvrecap  13218  dvef  13229  reeff1olem  13233  pilem3  13245  ptolemy  13286  rplogcl  13341  rpcxpef  13356  cxprec  13372  rpcxproot  13375  rplogb1  13407  logbgt0b  13425  logbgcd1irr  13426  binom4  13438  bj-nnan  13454  bj-indind  13649  bj-omtrans  13673  bj-inf2vnlem1  13687  sscoll2  13705  pwtrufal  13711  sssneq  13716  pw1nct  13717  nninfsellemsuc  13726  nninfomnilem  13732  exmidsbthrlem  13735  qdencn  13740  trilpo  13756  trirec0  13757  apdiff  13761  iswomninnlem  13762  iswomni0  13764  redcwlpo  13768  redc0  13770  reap0  13771  dceqnconst  13772  dcapnconst  13773  neapmkv  13780