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

This theorem is referenced by:  tfr2b  8347  rdgdmlim  8368  oeoa  8549  oeoe  8551  ordtypelem3  9465  ordtypelem5  9467  ordtypelem6  9468  ordtypelem7  9469  ordtypelem9  9471  r1fin  9718  r1tr  9721  r1ordg  9723  r1ord3g  9724  r1pwss  9729  r1val1  9731  rankwflemb  9738  r1elwf  9741  rankr1ai  9743  rankdmr1  9746  rankr1ag  9747  rankr1bg  9748  pwwf  9752  unwf  9755  rankr1clem  9765  rankr1c  9766  rankval3b  9771  rankonidlem  9773  onssr1  9776  rankeq0b  9805  alephsuc2  10025  ackbij2  10188  wunom  10665  negiso  12144  infrenegsup  12147  om2uzoi  13870  faclbnd4lem1  14203  hashunlei  14335  hashsslei  14336  hashle2pr  14388  cos01bnd  16079  cos1bnd  16080  cos2bnd  16081  sincos2sgn  16087  sin4lt0  16088  egt2lt3  16099  divalglem9  16294  bitsinv  16339  drngui  20231  srasca  20705  cnfldfunALT  20846  redvr  21058  refld  21060  iccpnfcnv  24344  xrhmph  24347  recvs  24546  recvsOLD  24547  qcvs  24548  i1f1  25091  itg11  25092  dvcos  25384  sinpi  25851  sinhalfpilem  25857  coshalfpi  25863  sincosq1lem  25891  tangtx  25899  sincos4thpi  25907  tan4thpi  25908  sincos6thpi  25909  sincos3rdpi  25910  pige3ALT  25913  logltb  25992  1cubrlem  26228  1cubr  26229  log2tlbnd  26332  cxploglim2  26365  emcllem6  26387  emcllem7  26388  ppiublem1  26587  ppiublem2  26588  bposlem9  26677  lgsdir2lem4  26713  lgsdir2lem5  26714  chebbnd1lem2  26855  chebbnd1lem3  26856  chebbnd1  26857  dchrvmasumlema  26885  mulog2sumlem2  26920  pntlemb  26982  qdrng  27005  upgrbi  28107  upgr1elem  28126  usgrexmpledg  28273  ntrl2v2e  29165  frgrwopreg2  29326  normlem7tALT  30124  hhsssh  30274  shintcli  30334  chintcli  30336  omlsi  30409  qlaxr3i  30641  lnophm  31024  nmcopex  31034  nmcoplb  31035  nmbdfnlbi  31054  nmcfnex  31058  nmcfnlb  31059  hmopidmch  31158  hmopidmpj  31159  chirred  31400  1fldgenq  32160  rrxdim  32396  xrge0hmph  32602  qqh0  32654  qqh1  32655  rerrext  32679  zrhre  32689  qqhre  32690  mbfmvolf  32955  hgt750lem  33353  subfacval2  33868  erdszelem5  33876  erdszelem6  33877  erdszelem7  33878  erdszelem8  33879  filnetlem3  34928  filnetlem4  34929  bj-genr  35147  bj-genl  35148  bj-genan  35149  3lexlogpow5ineq5  40590  aks4d1p1p7  40604  acos1half  40695  uun0.1  43182  pssnssi  43433  fourierdlem62  44529  fourierdlem68  44535  abcdtb  45281  abcdtc  45282  abcdtd  45283  nabctnabc  45286  zlmodzxzsubm  46555  zlmodzxzldep  46705  ldepsnlinclem1  46706  ldepsnlinclem2  46707  sepfsepc  47080  prstcleval  47208  prstcocval  47211