Theorem simpri 486

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

Syntax hints:   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  exanOLD  1845  tfr2b  7887  rdgdmlim  7908  oeoa  8076  oeoe  8078  ordtypelem3  8833  ordtypelem5  8835  ordtypelem6  8836  ordtypelem7  8837  ordtypelem9  8839  r1fin  9051  r1tr  9054  r1ordg  9056  r1ord3g  9057  r1pwss  9062  r1val1  9064  rankwflemb  9071  r1elwf  9074  rankr1ai  9076  rankdmr1  9079  rankr1ag  9080  rankr1bg  9081  pwwf  9085  unwf  9088  rankr1clem  9098  rankr1c  9099  rankval3b  9104  rankonidlem  9106  onssr1  9109  rankeq0b  9138  alephsuc2  9355  ackbij2  9514  wunom  9991  negiso  11471  infrenegsup  11474  om2uzoi  13173  faclbnd4lem1  13503  hashunlei  13634  hashsslei  13635  hashle2pr  13681  cos01bnd  15372  cos1bnd  15373  cos2bnd  15374  sincos2sgn  15380  sin4lt0  15381  egt2lt3  15392  divalglem9  15585  bitsinv  15630  drngui  19198  redvr  20443  refld  20445  recrng  20447  iccpnfcnv  23231  xrhmph  23234  recvs  23433  qcvs  23434  i1f1  23974  itg11  23975  dvcos  24263  sinpi  24726  sinhalfpilem  24732  coshalfpi  24738  sincosq1lem  24766  tangtx  24774  sincos4thpi  24782  tan4thpi  24783  sincos6thpi  24784  sincos3rdpi  24785  pige3ALT  24788  logltb  24864  1cubrlem  25100  1cubr  25101  log2tlbnd  25205  cxploglim2  25238  emcllem6  25260  emcllem7  25261  ppiublem1  25460  ppiublem2  25461  bposlem9  25550  lgsdir2lem4  25586  lgsdir2lem5  25587  chebbnd1lem2  25728  chebbnd1lem3  25729  chebbnd1  25730  dchrvmasumlema  25758  mulog2sumlem2  25793  pntlemb  25855  qdrng  25878  upgrbi  26561  upgr1elem  26580  usgrexmpledg  26727  ntrl2v2e  27619  frgrwopreg2  27782  normlem7tALT  28579  hhsssh  28729  shintcli  28789  chintcli  28791  omlsi  28864  qlaxr3i  29096  lnophm  29479  nmcopex  29489  nmcoplb  29490  nmbdfnlbi  29509  nmcfnex  29513  nmcfnlb  29514  hmopidmch  29613  hmopidmpj  29614  chirred  29855  rrxdim  30608  xrge0hmph  30784  qqh0  30834  qqh1  30835  rerrext  30859  zrhre  30869  qqhre  30870  mbfmvolf  31133  hgt750lem  31531  subfacval2  32036  erdszelem5  32044  erdszelem6  32045  erdszelem7  32046  erdszelem8  32047  filnetlem3  33331  filnetlem4  33332  bj-genr  33543  bj-genl  33544  bj-genan  33545  uun0.1  40664  pssnssi  40920  fourierdlem62  42009  fourierdlem68  42015  abcdtb  42717  abcdtc  42718  abcdtd  42719  nabctnabc  42722  zlmodzxzsubm  43899  zlmodzxzldep  44053  ldepsnlinclem1  44054  ldepsnlinclem2  44055