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  8388  rdgfun  8408  oeoa  8590  oeoe  8592  ssdomg  9011  ordtypelem4  9499  ordtypelem6  9501  ordtypelem7  9502  infxpenlem  10073  mulnzcnf  11943  negiso  12278  infrenegsup  12281  hashunlei  14550  hashsslei  14551  cos01bnd  16334  cos1bnd  16335  cos2bnd  16336  sin4lt0  16343  egt2lt3  16354  epos  16355  ene1  16358  divalglem5  16547  bitsf1o  16595  gcdaddmlem  16676  sravsca  21436  zrhpsgnmhm  21870  resubgval  21895  re1r  21899  redvr  21903  refld  21905  rzgrp  21909  txindis  23933  icopnfhmeo  25244  iccpnfcnv  25245  iccpnfhmeo  25246  xrhmeo  25247  cnheiborlem  25255  recvs  25447  qcvs  25448  rrxcph  25693  volf  25830  i1f1  25991  itg11  25992  dvsin  26282  taylthlem2  26683  reefgim  26759  pilem3  26762  pigt2lt4  26763  pire  26765  pipos  26769  sinhalfpi  26779  tan4thpi  26825  sincos3rdpi  26827  pigt3  26828  circgrp  26862  circsubm  26863  1cubrlem  27151  1cubr  27152  jensenlem2  27297  amgmlem  27299  emcllem6  27310  emcllem7  27311  harmonicbnd3  27317  ppiublem1  27511  chtub  27521  bposlem7  27599  lgsdir2lem4  27637  lgsdir2lem5  27638  chebbnd1  27781  mulog2sumlem2  27844  pntpbnd1a  27894  pntpbnd2  27896  pntlemb  27906  pntlemk  27915  qrng0  27930  qrng1  27931  qrngneg  27932  qrngdiv  27933  qabsabv  27938  ex-sqrt  31037  normlem7tALT  31703  hhsssh  31853  shintcli  31913  chintcli  31915  omlsi  31988  qlaxr3i  32220  lnophm  32603  nmcopex  32613  nmcoplb  32614  nmbdfnlbi  32633  nmcfnex  32637  nmcfnlb  32638  hmopidmch  32737  hmopidmpj  32738  chirred  32979  threehalves  33463  qfld  33841  1fldgenq  33866  nn0archi  33890  ccfldextrr  34260  ccfldsrarelvec  34285  constrextdg2  34363  constrext2chnlem  34364  constrcon  34388  2sqr3minply  34394  2sqr3nconstr  34395  cos9thpiminplylem6  34401  cos9thpiminply  34402  cos9thpinconstrlem2  34404  trisecnconstr  34406  xrge0iifiso  34549  xrge0iifmhm  34553  xrge0pluscn  34554  rezh  34583  qqh0  34598  qqh1  34599  qqhcn  34605  qqhucn  34606  rerrext  34623  cnrrext  34624  mbfmvolf  34881  hgt750lem  35263  subfacval3  35923  erdszelem5  35929  erdszelem8  35932  filnetlem3  37138  filnetlem4  37139  bj-genr  37447  bj-genl  37448  bj-genan  37449  bj-rveccmod  38191  reheibor  38741  cossssid  39457  eqvrelcoss3  39602  3lexlogpow5ineq5  43078  aks6d1c7lem1  43198  tan3rdpi  43371  sin2t3rdpi  43372  sin4t3rdpi  43374  asin1half  43376  fourierdlem68  47128  fourierdlem77  47137  fourierdlem80  47140  fouriersw  47185  etransclem23  47211  gsumge0cl  47325  numtowerdt  47860  abcdta  47939  abcdtb  47940  abcdtc  47941  nabctnabc  47945  ppivalnn4  48656  zlmodzxzsubm  49415  zlmodzxzldeplem3  49558  ldepsnlinclem1  49561  ldepsnlinclem2  49562  ldepsnlinc  49564  sepfsepc  49980  prstcleval  50607  prstcocval  50609  setc1onsubc  50654  empty-surprise  50822  veroquadmodzerod  50928  veroquadnolindfd  50929  veroquaddetzerod  50930  amgmwlem  50931  amgmlemALT  50932