Theorem simpri 489

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

Hypothesis

Ref	Expression
simpri.1	⊢ (𝜑 ∧ 𝜓)

Assertion

Ref	Expression
simpri	⊢ 𝜓

Proof of Theorem simpri

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

Syntax hints:   ∧ wa 399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 400

This theorem is referenced by:  tfr2b  8132  rdgdmlim  8153  oeoa  8325  oeoe  8327  ordtypelem3  9136  ordtypelem5  9138  ordtypelem6  9139  ordtypelem7  9140  ordtypelem9  9142  r1fin  9389  r1tr  9392  r1ordg  9394  r1ord3g  9395  r1pwss  9400  r1val1  9402  rankwflemb  9409  r1elwf  9412  rankr1ai  9414  rankdmr1  9417  rankr1ag  9418  rankr1bg  9419  pwwf  9423  unwf  9426  rankr1clem  9436  rankr1c  9437  rankval3b  9442  rankonidlem  9444  onssr1  9447  rankeq0b  9476  alephsuc2  9694  ackbij2  9857  wunom  10334  negiso  11812  infrenegsup  11815  om2uzoi  13528  faclbnd4lem1  13859  hashunlei  13992  hashsslei  13993  hashle2pr  14043  cos01bnd  15747  cos1bnd  15748  cos2bnd  15749  sincos2sgn  15755  sin4lt0  15756  egt2lt3  15767  divalglem9  15962  bitsinv  16007  drngui  19773  redvr  20579  refld  20581  recrng  20583  iccpnfcnv  23841  xrhmph  23844  recvs  24043  qcvs  24044  i1f1  24587  itg11  24588  dvcos  24880  sinpi  25347  sinhalfpilem  25353  coshalfpi  25359  sincosq1lem  25387  tangtx  25395  sincos4thpi  25403  tan4thpi  25404  sincos6thpi  25405  sincos3rdpi  25406  pige3ALT  25409  logltb  25488  1cubrlem  25724  1cubr  25725  log2tlbnd  25828  cxploglim2  25861  emcllem6  25883  emcllem7  25884  ppiublem1  26083  ppiublem2  26084  bposlem9  26173  lgsdir2lem4  26209  lgsdir2lem5  26210  chebbnd1lem2  26351  chebbnd1lem3  26352  chebbnd1  26353  dchrvmasumlema  26381  mulog2sumlem2  26416  pntlemb  26478  qdrng  26501  upgrbi  27184  upgr1elem  27203  usgrexmpledg  27350  ntrl2v2e  28241  frgrwopreg2  28402  normlem7tALT  29200  hhsssh  29350  shintcli  29410  chintcli  29412  omlsi  29485  qlaxr3i  29717  lnophm  30100  nmcopex  30110  nmcoplb  30111  nmbdfnlbi  30130  nmcfnex  30134  nmcfnlb  30135  hmopidmch  30234  hmopidmpj  30235  chirred  30476  rrxdim  31411  xrge0hmph  31596  qqh0  31646  qqh1  31647  rerrext  31671  zrhre  31681  qqhre  31682  mbfmvolf  31945  hgt750lem  32343  subfacval2  32862  erdszelem5  32870  erdszelem6  32871  erdszelem7  32872  erdszelem8  32873  filnetlem3  34306  filnetlem4  34307  bj-genr  34525  bj-genl  34526  bj-genan  34527  3lexlogpow5ineq5  39802  aks4d1p1p7  39815  acos1half  39892  uun0.1  42071  pssnssi  42324  fourierdlem62  43384  fourierdlem68  43390  abcdtb  44093  abcdtc  44094  abcdtd  44095  nabctnabc  44098  zlmodzxzsubm  45368  zlmodzxzldep  45518  ldepsnlinclem1  45519  ldepsnlinclem2  45520  sepfsepc  45894