Theorem simpli 489

Description: Inference eliminating a conjunct. (Contributed by NM, 15-Jun-1994.)

Hypothesis

Ref	Expression
simpli.1	⊢ (𝜑 ∧ 𝜓)

Assertion

Ref	Expression
simpli	⊢ 𝜑

Proof of Theorem simpli

Step	Hyp	Ref	Expression
1		simpli.1	. 2 ⊢ (𝜑 ∧ 𝜓)
2		simpl 488	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
3	1, 2	ax-mp 5	1 ⊢ 𝜑

This proof depends on syntax axioms:   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  tfr2b  8408  rdgfun  8428  oeoa  8610  oeoe  8612  ssdomg  9031  ordtypelem4  9519  ordtypelem6  9521  ordtypelem7  9522  infxpenlem  10096  mulnzcnf  11966  negiso  12301  infrenegsup  12304  hashunlei  14574  hashsslei  14575  cos01bnd  16360  cos1bnd  16361  cos2bnd  16362  sin4lt0  16369  egt2lt3  16380  epos  16381  ene1  16384  divalglem5  16573  bitsf1o  16621  gcdaddmlem  16702  sravsca  21462  zrhpsgnmhm  21896  resubgval  21921  re1r  21925  redvr  21929  refld  21931  rzgrp  21935  txindis  23959  icopnfhmeo  25270  iccpnfcnv  25271  iccpnfhmeo  25272  xrhmeo  25273  cnheiborlem  25281  recvs  25473  qcvs  25474  rrxcph  25719  volf  25856  i1f1  26017  itg11  26018  dvsin  26308  taylthlem2  26707  reefgim  26783  pilem3  26786  pigt2lt4  26787  pire  26789  pipos  26793  sinhalfpi  26803  tan4thpi  26849  sincos3rdpi  26851  pigt3  26852  circgrp  26886  circsubm  26887  1cubrlem  27175  1cubr  27176  jensenlem2  27321  amgmlem  27323  emcllem6  27334  emcllem7  27335  harmonicbnd3  27341  ppiublem1  27535  chtub  27545  bposlem7  27623  lgsdir2lem4  27661  lgsdir2lem5  27662  chebbnd1  27805  mulog2sumlem2  27868  pntpbnd1a  27918  pntpbnd2  27920  pntlemb  27930  pntlemk  27939  qrng0  27954  qrng1  27955  qrngneg  27956  qrngdiv  27957  qabsabv  27962  ex-sqrt  31061  normlem7tALT  31727  hhsssh  31877  shintcli  31937  chintcli  31939  omlsi  32012  qlaxr3i  32244  lnophm  32627  nmcopex  32637  nmcoplb  32638  nmbdfnlbi  32657  nmcfnex  32661  nmcfnlb  32662  hmopidmch  32761  hmopidmpj  32762  chirred  33003  threehalves  33528  qfld  33906  1fldgenq  33931  nn0archi  33955  ccfldextrr  34325  ccfldsrarelvec  34350  constrextdg2  34428  constrext2chnlem  34429  constrcon  34453  2sqr3minply  34459  2sqr3nconstr  34460  cos9thpiminplylem6  34466  cos9thpiminply  34467  cos9thpinconstrlem2  34469  trisecnconstr  34471  xrge0iifiso  34614  xrge0iifmhm  34618  xrge0pluscn  34619  rezh  34648  qqh0  34663  qqh1  34664  qqhcn  34670  qqhucn  34671  rerrext  34688  cnrrext  34689  mbfmvolf  34945  hgt750lem  35327  subfacval3  36041  erdszelem5  36047  erdszelem8  36050  filnetlem3  37261  filnetlem4  37262  bj-genr  37570  bj-genl  37571  bj-genan  37572  bj-rveccmod  38317  reheibor  38867  cossssid  39583  eqvrelcoss3  39728  3lexlogpow5ineq5  43204  aks6d1c7lem1  43324  tan3rdpi  43497  sin2t3rdpi  43498  sin4t3rdpi  43500  asin1half  43502  fourierdlem68  47278  fourierdlem77  47287  fourierdlem80  47290  fouriersw  47335  etransclem23  47361  gsumge0cl  47475  numtowerdt  48010  abcdta  48089  abcdtb  48090  abcdtc  48091  nabctnabc  48095  ppivalnn4  48806  zlmodzxzsubm  49565  zlmodzxzldeplem3  49708  ldepsnlinclem1  49711  ldepsnlinclem2  49712  ldepsnlinc  49714  sepfsepc  50136  prstcleval  50787  prstcocval  50789  setc1onsubc  50834  par2cat  50862  parswapfunc  50872  par2diag  50874  fuconuniqlem  50875  fuconuniqvalslem  50877  empty-surprise  51047  veroquadmodzerod  51153  veroquadnolindfd  51154  veroquaddetzerod  51155  amgmwlem  51156  amgmlemALT  51157