Theorem simpri 488

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 487	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
3	1, 2	ax-mp 5	1 ⊢ 𝜓

Syntax hints:   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  exanOLD  1859  tfr2b  8026  rdgdmlim  8047  oeoa  8217  oeoe  8219  ordtypelem3  8978  ordtypelem5  8980  ordtypelem6  8981  ordtypelem7  8982  ordtypelem9  8984  r1fin  9196  r1tr  9199  r1ordg  9201  r1ord3g  9202  r1pwss  9207  r1val1  9209  rankwflemb  9216  r1elwf  9219  rankr1ai  9221  rankdmr1  9224  rankr1ag  9225  rankr1bg  9226  pwwf  9230  unwf  9233  rankr1clem  9243  rankr1c  9244  rankval3b  9249  rankonidlem  9251  onssr1  9254  rankeq0b  9283  alephsuc2  9500  ackbij2  9659  wunom  10136  negiso  11615  infrenegsup  11618  om2uzoi  13317  faclbnd4lem1  13647  hashunlei  13780  hashsslei  13781  hashle2pr  13829  cos01bnd  15533  cos1bnd  15534  cos2bnd  15535  sincos2sgn  15541  sin4lt0  15542  egt2lt3  15553  divalglem9  15746  bitsinv  15791  drngui  19502  redvr  20755  refld  20757  recrng  20759  iccpnfcnv  23542  xrhmph  23545  recvs  23744  qcvs  23745  i1f1  24285  itg11  24286  dvcos  24574  sinpi  25037  sinhalfpilem  25043  coshalfpi  25049  sincosq1lem  25077  tangtx  25085  sincos4thpi  25093  tan4thpi  25094  sincos6thpi  25095  sincos3rdpi  25096  pige3ALT  25099  logltb  25177  1cubrlem  25413  1cubr  25414  log2tlbnd  25517  cxploglim2  25550  emcllem6  25572  emcllem7  25573  ppiublem1  25772  ppiublem2  25773  bposlem9  25862  lgsdir2lem4  25898  lgsdir2lem5  25899  chebbnd1lem2  26040  chebbnd1lem3  26041  chebbnd1  26042  dchrvmasumlema  26070  mulog2sumlem2  26105  pntlemb  26167  qdrng  26190  upgrbi  26872  upgr1elem  26891  usgrexmpledg  27038  ntrl2v2e  27931  frgrwopreg2  28092  normlem7tALT  28890  hhsssh  29040  shintcli  29100  chintcli  29102  omlsi  29175  qlaxr3i  29407  lnophm  29790  nmcopex  29800  nmcoplb  29801  nmbdfnlbi  29820  nmcfnex  29824  nmcfnlb  29825  hmopidmch  29924  hmopidmpj  29925  chirred  30166  rrxdim  31007  xrge0hmph  31170  qqh0  31220  qqh1  31221  rerrext  31245  zrhre  31255  qqhre  31256  mbfmvolf  31519  hgt750lem  31917  subfacval2  32429  erdszelem5  32437  erdszelem6  32438  erdszelem7  32439  erdszelem8  32440  filnetlem3  33723  filnetlem4  33724  bj-genr  33935  bj-genl  33936  bj-genan  33937  uun0.1  41105  pssnssi  41360  fourierdlem62  42447  fourierdlem68  42453  abcdtb  43156  abcdtc  43157  abcdtd  43158  nabctnabc  43161  zlmodzxzsubm  44401  zlmodzxzldep  44553  ldepsnlinclem1  44554  ldepsnlinclem2  44555