Theorem simpri 484

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

Syntax hints:   ∧ wa 394

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 395

This theorem is referenced by:  tfr2b  8426  rdgdmlim  8447  oeoa  8627  oeoe  8629  ordtypelem3  9563  ordtypelem5  9565  ordtypelem6  9566  ordtypelem7  9567  ordtypelem9  9569  r1fin  9816  r1tr  9819  r1ordg  9821  r1ord3g  9822  r1pwss  9827  r1val1  9829  rankwflemb  9836  r1elwf  9839  rankr1ai  9841  rankdmr1  9844  rankr1ag  9845  rankr1bg  9846  pwwf  9850  unwf  9853  rankr1clem  9863  rankr1c  9864  rankval3b  9869  rankonidlem  9871  onssr1  9874  rankeq0b  9903  alephsuc2  10123  ackbij2  10286  wunom  10763  negiso  12246  infrenegsup  12249  om2uzoi  13975  faclbnd4lem1  14310  hashunlei  14442  hashsslei  14443  hashle2pr  14496  cos01bnd  16188  cos1bnd  16189  cos2bnd  16190  sincos2sgn  16196  sin4lt0  16197  egt2lt3  16208  divalglem9  16403  bitsinv  16448  drngui  20713  srasca  21162  cnfldfunALT  21358  cnfldfunALTOLD  21371  redvr  21613  refld  21615  iccpnfcnv  24960  xrhmph  24963  recvs  25164  recvsOLD  25165  qcvs  25166  i1f1  25710  itg11  25711  dvcos  26006  sinpi  26485  sinhalfpilem  26491  coshalfpi  26497  sincosq1lem  26525  tangtx  26533  sincos4thpi  26541  tan4thpi  26542  sincos6thpi  26543  sincos3rdpi  26544  pige3ALT  26547  logltb  26627  1cubrlem  26869  1cubr  26870  log2tlbnd  26973  cxploglim2  27007  emcllem6  27029  emcllem7  27030  ppiublem1  27231  ppiublem2  27232  bposlem9  27321  lgsdir2lem4  27357  lgsdir2lem5  27358  chebbnd1lem2  27499  chebbnd1lem3  27500  chebbnd1  27501  dchrvmasumlema  27529  mulog2sumlem2  27564  pntlemb  27626  qdrng  27649  upgrbi  29029  upgr1elem  29048  usgrexmpledg  29198  ntrl2v2e  30091  frgrwopreg2  30252  normlem7tALT  31052  hhsssh  31202  shintcli  31262  chintcli  31264  omlsi  31337  qlaxr3i  31569  lnophm  31952  nmcopex  31962  nmcoplb  31963  nmbdfnlbi  31982  nmcfnex  31986  nmcfnlb  31987  hmopidmch  32086  hmopidmpj  32087  chirred  32328  1fldgenq  33172  zringfrac  33429  rrxdim  33509  2sqr3minply  33607  xrge0hmph  33747  qqh0  33799  qqh1  33800  rerrext  33824  zrhre  33834  qqhre  33835  mbfmvolf  34100  hgt750lem  34497  subfacval2  35015  erdszelem5  35023  erdszelem6  35024  erdszelem7  35025  erdszelem8  35026  filnetlem3  36092  filnetlem4  36093  bj-genr  36311  bj-genl  36312  bj-genan  36313  3lexlogpow5ineq5  41759  aks4d1p1p7  41773  acos1half  42328  uun0.1  44454  pssnssi  44702  fourierdlem62  45789  fourierdlem68  45795  abcdtb  46541  abcdtc  46542  abcdtd  46543  nabctnabc  46546  zlmodzxzsubm  47738  zlmodzxzldep  47887  ldepsnlinclem1  47888  ldepsnlinclem2  47889  sepfsepc  48261  prstcleval  48389  prstcocval  48392