Theorem simpri 490

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

Syntax hints:   ∧ wa 400

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 401

This theorem is referenced by:  tfr2b  8371  rdgdmlim  8392  oeoa  8571  oeoe  8573  ordtypelem3  9470  ordtypelem5  9472  ordtypelem6  9473  ordtypelem7  9474  ordtypelem9  9476  r1fin  9733  r1tr  9736  r1ordg  9738  r1ord3g  9739  r1pwss  9744  r1val1  9746  rankwflemb  9753  r1elwf  9756  rankr1ai  9758  rankdmr1  9761  rankr1ag  9762  rankr1bg  9763  pwwf  9767  unwf  9770  rankr1clem  9780  rankr1c  9781  rankval3b  9786  rankonidlem  9788  onssr1  9791  rankeq0b  9820  alephsuc2  10052  ackbij2  10213  wunom  10693  negiso  12186  infrenegsup  12189  om2uzoi  13982  faclbnd4lem1  14320  hashunlei  14452  hashsslei  14453  hashle2pr  14504  cos01bnd  16232  cos1bnd  16233  cos2bnd  16234  sincos2sgn  16240  sin4lt0  16241  egt2lt3  16252  divalglem9  16449  bitsinv  16496  drngui  20810  srasca  21270  cnfldfunALT  21497  redvr  21727  refld  21729  iccpnfcnv  25064  xrhmph  25067  recvs  25266  qcvs  25267  i1f1  25810  itg11  25811  dvcos  26103  sinpi  26576  sinhalfpilem  26586  coshalfpi  26592  sincosq1lem  26620  tangtx  26628  sincos4thpi  26636  tan4thpi  26637  tan4thpiOLD  26638  sincos6thpi  26639  sincos3rdpi  26640  pige3ALT  26643  logltb  26723  1cubrlem  26964  1cubr  26965  log2tlbnd  27068  cxploglim2  27101  emcllem6  27123  emcllem7  27124  ppiublem1  27324  ppiublem2  27325  bposlem9  27414  lgsdir2lem4  27450  lgsdir2lem5  27451  chebbnd1lem2  27592  chebbnd1lem3  27593  chebbnd1  27594  dchrvmasumlema  27622  mulog2sumlem2  27657  pntlemb  27719  qdrng  27742  upgrbi  29352  upgr1elem  29371  usgrexmpledg  29521  ntrl2v2e  30418  frgrwopreg2  30579  normlem7tALT  31380  hhsssh  31530  shintcli  31590  chintcli  31592  omlsi  31665  qlaxr3i  31897  lnophm  32280  nmcopex  32290  nmcoplb  32291  nmbdfnlbi  32310  nmcfnex  32314  nmcfnlb  32315  hmopidmch  32414  hmopidmpj  32415  chirred  32656  1fldgenq  33558  zringfrac  33761  esplyind  33882  rrxdim  33921  constrextdg2  34056  constrext2chnlem  34057  2sqr3minply  34087  2sqr3nconstr  34088  cos9thpiminply  34095  cos9thpinconstrlem2  34097  trisecnconstr  34099  xrge0hmph  34239  qqh0  34291  qqh1  34292  rerrext  34316  zrhre  34326  qqhre  34327  mbfmvolf  34573  hgt750lem  34955  r11  35402  r12  35403  subfacval2  35550  erdszelem5  35558  erdszelem6  35559  erdszelem7  35560  erdszelem8  35561  filnetlem3  36753  filnetlem4  36754  bj-genr  37062  bj-genl  37063  bj-genan  37064  3lexlogpow5ineq5  42689  aks4d1p1p7  42703  tan3rdpi  42973  cos2t3rdpi  42975  cos4t3rdpi  42977  acos1half  42979  uun0.1  45351  permaxpow  45583  pssnssi  45677  fourierdlem62  46740  fourierdlem68  46746  nthrucw  47460  abcdtb  47518  abcdtc  47519  abcdtd  47520  nabctnabc  47523  zlmodzxzsubm  48990  zlmodzxzldep  49135  ldepsnlinclem1  49136  ldepsnlinclem2  49137  sepfsepc  49557  idfth  49787  idsubc  49789  prstcleval  50184  prstcocval  50186  setc1onsubc  50231