Theorem simpri 477

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

Syntax hints:   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  exan  1775  exanOLD  1776  exanOLDOLD  2155  tfr2b  7379  rdgdmlim  7400  oeoa  7564  oeoe  7566  ordtypelem3  8308  ordtypelem5  8310  ordtypelem6  8311  ordtypelem7  8312  ordtypelem9  8314  r1fin  8519  r1tr  8522  r1ordg  8524  r1ord3g  8525  r1pwss  8530  r1val1  8532  rankwflemb  8539  r1elwf  8542  rankr1ai  8544  rankdmr1  8547  rankr1ag  8548  rankr1bg  8549  pwwf  8553  unwf  8556  rankr1clem  8566  rankr1c  8567  rankval3b  8572  rankonidlem  8574  onssr1  8577  rankeq0b  8606  alephsuc2  8786  ackbij2  8948  wunom  9421  negiso  10880  infrenegsup  10883  om2uzoi  12616  faclbnd4lem1  12942  hashunlei  13072  hashsslei  13073  cos01bnd  14755  cos1bnd  14756  cos2bnd  14757  sincos2sgn  14763  sin4lt0  14764  egt2lt3  14773  divalglem9  14962  bitsinv  15008  strlemor1  15796  drngui  18576  redvr  19782  refld  19784  recrng  19786  iccpnfcnv  22551  xrhmph  22554  recvs  22754  qcvs  22755  i1f1  23263  itg11  23264  dvcos  23550  sinpi  24013  sinhalfpilem  24019  coshalfpi  24025  sincosq1lem  24053  tangtx  24061  sincos4thpi  24069  tan4thpi  24070  sincos6thpi  24071  sincos3rdpi  24072  pige3  24073  logltb  24150  1cubrlem  24368  1cubr  24369  log2tlbnd  24472  cxploglim2  24505  emcllem6  24527  emcllem7  24528  ppiublem1  24727  ppiublem2  24728  bposlem9  24817  lgsdir2lem4  24853  lgsdir2lem5  24854  chebbnd1lem2  24959  chebbnd1lem3  24960  chebbnd1  24961  dchrvmasumlema  24989  mulog2sumlem2  25024  pntlemb  25086  qdrng  25109  upgrbi  25760  upgr1elem  25778  umgra1  25855  uslgra1  25901  2trllemE  26083  umgrabi  26510  normlem7tALT  27360  hhsssh  27510  shintcli  27572  chintcli  27574  omlsi  27647  qlaxr3i  27879  lnophm  28262  nmcopex  28272  nmcoplb  28273  nmbdfnlbi  28292  nmcfnex  28296  nmcfnlb  28297  hmopidmch  28396  hmopidmpj  28397  chirred  28638  xrge0hmph  29306  qqh0  29356  qqh1  29357  rerrext  29381  zrhre  29391  qqhre  29392  mbfmvolf  29655  subfacval2  30423  erdszelem5  30431  erdszelem6  30432  erdszelem7  30433  erdszelem8  30434  filnetlem3  31545  filnetlem4  31546  bj-genr  31776  bj-genl  31777  bj-genan  31778  uun0.1  38026  pssnssi  38312  fourierdlem62  39061  fourierdlem68  39067  abcdtb  39742  abcdtc  39743  abcdtd  39744  nabctnabc  39747  usgrexmpledg  40486  ntrl2v2e  41325  frgrwopreg2  41488  zlmodzxzsubm  41930  zlmodzxzldep  42087  ldepsnlinclem1  42088  ldepsnlinclem2  42089