Theorem simpri 475

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

Syntax hints:   ∧ wa 384

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

This theorem is referenced by:  exan  1948  exanOLD  1949  tfr2b  7724  rdgdmlim  7745  oeoa  7910  oeoe  7912  ordtypelem3  8660  ordtypelem5  8662  ordtypelem6  8663  ordtypelem7  8664  ordtypelem9  8666  r1fin  8879  r1tr  8882  r1ordg  8884  r1ord3g  8885  r1pwss  8890  r1val1  8892  rankwflemb  8899  r1elwf  8902  rankr1ai  8904  rankdmr1  8907  rankr1ag  8908  rankr1bg  8909  pwwf  8913  unwf  8916  rankr1clem  8926  rankr1c  8927  rankval3b  8932  rankonidlem  8934  onssr1  8937  rankeq0b  8966  alephsuc2  9182  ackbij2  9346  wunom  9823  negiso  11284  infrenegsup  11287  om2uzoi  12974  faclbnd4lem1  13296  hashunlei  13425  hashsslei  13426  hashle2pr  13472  cos01bnd  15132  cos1bnd  15133  cos2bnd  15134  sincos2sgn  15140  sin4lt0  15141  egt2lt3  15150  divalglem9  15340  bitsinv  15385  strlemor1OLD  16176  drngui  18953  redvr  20168  refld  20170  recrng  20172  iccpnfcnv  22953  xrhmph  22956  recvs  23155  qcvs  23156  i1f1  23670  itg11  23671  dvcos  23959  sinpi  24423  sinhalfpilem  24429  coshalfpi  24435  sincosq1lem  24463  tangtx  24471  sincos4thpi  24479  tan4thpi  24480  sincos6thpi  24481  sincos3rdpi  24482  pige3  24483  logltb  24559  1cubrlem  24781  1cubr  24782  log2tlbnd  24885  cxploglim2  24918  emcllem6  24940  emcllem7  24941  ppiublem1  25140  ppiublem2  25141  bposlem9  25230  lgsdir2lem4  25266  lgsdir2lem5  25267  chebbnd1lem2  25372  chebbnd1lem3  25373  chebbnd1  25374  dchrvmasumlema  25402  mulog2sumlem2  25437  pntlemb  25499  qdrng  25522  upgrbi  26201  upgr1elem  26220  usgrexmpledg  26369  ntrl2v2e  27330  frgrwopreg2  27493  normlem7tALT  28303  hhsssh  28453  shintcli  28515  chintcli  28517  omlsi  28590  qlaxr3i  28822  lnophm  29205  nmcopex  29215  nmcoplb  29216  nmbdfnlbi  29235  nmcfnex  29239  nmcfnlb  29240  hmopidmch  29339  hmopidmpj  29340  chirred  29581  xrge0hmph  30302  qqh0  30352  qqh1  30353  rerrext  30377  zrhre  30387  qqhre  30388  mbfmvolf  30652  hgt750lem  31053  subfacval2  31490  erdszelem5  31498  erdszelem6  31499  erdszelem7  31500  erdszelem8  31501  filnetlem3  32694  filnetlem4  32695  bj-genr  32904  bj-genl  32905  bj-genan  32906  uun0.1  39499  pssnssi  39772  fourierdlem62  40861  fourierdlem68  40867  abcdtb  41572  abcdtc  41573  abcdtd  41574  nabctnabc  41577  zlmodzxzsubm  42702  zlmodzxzldep  42858  ldepsnlinclem1  42859  ldepsnlinclem2  42860