Theorem simpri 487

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

Syntax hints:   ∧ wa 397

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 398

This theorem is referenced by:  tfr2b  8396  rdgdmlim  8417  oeoa  8597  oeoe  8599  ordtypelem3  9515  ordtypelem5  9517  ordtypelem6  9518  ordtypelem7  9519  ordtypelem9  9521  r1fin  9768  r1tr  9771  r1ordg  9773  r1ord3g  9774  r1pwss  9779  r1val1  9781  rankwflemb  9788  r1elwf  9791  rankr1ai  9793  rankdmr1  9796  rankr1ag  9797  rankr1bg  9798  pwwf  9802  unwf  9805  rankr1clem  9815  rankr1c  9816  rankval3b  9821  rankonidlem  9823  onssr1  9826  rankeq0b  9855  alephsuc2  10075  ackbij2  10238  wunom  10715  negiso  12194  infrenegsup  12197  om2uzoi  13920  faclbnd4lem1  14253  hashunlei  14385  hashsslei  14386  hashle2pr  14438  cos01bnd  16129  cos1bnd  16130  cos2bnd  16131  sincos2sgn  16137  sin4lt0  16138  egt2lt3  16149  divalglem9  16344  bitsinv  16389  drngui  20363  srasca  20798  cnfldfunALT  20957  redvr  21170  refld  21172  iccpnfcnv  24460  xrhmph  24463  recvs  24662  recvsOLD  24663  qcvs  24664  i1f1  25207  itg11  25208  dvcos  25500  sinpi  25967  sinhalfpilem  25973  coshalfpi  25979  sincosq1lem  26007  tangtx  26015  sincos4thpi  26023  tan4thpi  26024  sincos6thpi  26025  sincos3rdpi  26026  pige3ALT  26029  logltb  26108  1cubrlem  26346  1cubr  26347  log2tlbnd  26450  cxploglim2  26483  emcllem6  26505  emcllem7  26506  ppiublem1  26705  ppiublem2  26706  bposlem9  26795  lgsdir2lem4  26831  lgsdir2lem5  26832  chebbnd1lem2  26973  chebbnd1lem3  26974  chebbnd1  26975  dchrvmasumlema  27003  mulog2sumlem2  27038  pntlemb  27100  qdrng  27123  upgrbi  28384  upgr1elem  28403  usgrexmpledg  28550  ntrl2v2e  29442  frgrwopreg2  29603  normlem7tALT  30403  hhsssh  30553  shintcli  30613  chintcli  30615  omlsi  30688  qlaxr3i  30920  lnophm  31303  nmcopex  31313  nmcoplb  31314  nmbdfnlbi  31333  nmcfnex  31337  nmcfnlb  31338  hmopidmch  31437  hmopidmpj  31438  chirred  31679  1fldgenq  32443  rrxdim  32730  xrge0hmph  32943  qqh0  32995  qqh1  32996  rerrext  33020  zrhre  33030  qqhre  33031  mbfmvolf  33296  hgt750lem  33694  subfacval2  34209  erdszelem5  34217  erdszelem6  34218  erdszelem7  34219  erdszelem8  34220  gg-cnfldfunALT  35229  filnetlem3  35313  filnetlem4  35314  bj-genr  35532  bj-genl  35533  bj-genan  35534  3lexlogpow5ineq5  40973  aks4d1p1p7  40987  acos1half  41463  uun0.1  43587  pssnssi  43838  fourierdlem62  44932  fourierdlem68  44938  abcdtb  45684  abcdtc  45685  abcdtd  45686  nabctnabc  45689  zlmodzxzsubm  47083  zlmodzxzldep  47233  ldepsnlinclem1  47234  ldepsnlinclem2  47235  sepfsepc  47608  prstcleval  47736  prstcocval  47739