Theorem simpri 486

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

Syntax hints:   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  tfr2b  8332  rdgdmlim  8353  oeoa  8530  oeoe  8532  ordtypelem3  9432  ordtypelem5  9434  ordtypelem6  9435  ordtypelem7  9436  ordtypelem9  9438  r1fin  9695  r1tr  9698  r1ordg  9700  r1ord3g  9701  r1pwss  9706  r1val1  9708  rankwflemb  9715  r1elwf  9718  rankr1ai  9720  rankdmr1  9723  rankr1ag  9724  rankr1bg  9725  pwwf  9729  unwf  9732  rankr1clem  9742  rankr1c  9743  rankval3b  9748  rankonidlem  9750  onssr1  9753  rankeq0b  9782  alephsuc2  10000  ackbij2  10162  wunom  10641  negiso  12134  infrenegsup  12137  om2uzoi  13915  faclbnd4lem1  14253  hashunlei  14385  hashsslei  14386  hashle2pr  14437  cos01bnd  16151  cos1bnd  16152  cos2bnd  16153  sincos2sgn  16159  sin4lt0  16160  egt2lt3  16171  divalglem9  16368  bitsinv  16415  drngui  20714  srasca  21177  cnfldfunALT  21369  redvr  21599  refld  21601  iccpnfcnv  24936  xrhmph  24939  recvs  25138  qcvs  25139  i1f1  25682  itg11  25683  dvcos  25975  sinpi  26445  sinhalfpilem  26452  coshalfpi  26458  sincosq1lem  26486  tangtx  26494  sincos4thpi  26502  tan4thpi  26503  tan4thpiOLD  26504  sincos6thpi  26505  sincos3rdpi  26506  pige3ALT  26509  logltb  26589  1cubrlem  26830  1cubr  26831  log2tlbnd  26934  cxploglim2  26967  emcllem6  26989  emcllem7  26990  ppiublem1  27190  ppiublem2  27191  bposlem9  27280  lgsdir2lem4  27316  lgsdir2lem5  27317  chebbnd1lem2  27458  chebbnd1lem3  27459  chebbnd1  27460  dchrvmasumlema  27488  mulog2sumlem2  27523  pntlemb  27585  qdrng  27608  upgrbi  29187  upgr1elem  29206  usgrexmpledg  29356  ntrl2v2e  30253  frgrwopreg2  30414  normlem7tALT  31215  hhsssh  31365  shintcli  31425  chintcli  31427  omlsi  31500  qlaxr3i  31732  lnophm  32115  nmcopex  32125  nmcoplb  32126  nmbdfnlbi  32145  nmcfnex  32149  nmcfnlb  32150  hmopidmch  32249  hmopidmpj  32250  chirred  32491  1fldgenq  33413  zringfrac  33644  esplyind  33766  rrxdim  33805  constrextdg2  33940  constrext2chnlem  33941  2sqr3minply  33971  2sqr3nconstr  33972  cos9thpiminply  33979  cos9thpinconstrlem2  33981  trisecnconstr  33983  xrge0hmph  34123  qqh0  34175  qqh1  34176  rerrext  34200  zrhre  34210  qqhre  34211  mbfmvolf  34457  hgt750lem  34842  r11  35284  r12  35285  subfacval2  35416  erdszelem5  35424  erdszelem6  35425  erdszelem7  35426  erdszelem8  35427  filnetlem3  36609  filnetlem4  36610  bj-genr  36919  bj-genl  36920  bj-genan  36921  3lexlogpow5ineq5  42546  aks4d1p1p7  42560  tan3rdpi  42830  cos2t3rdpi  42832  cos4t3rdpi  42834  acos1half  42836  uun0.1  45222  permaxpow  45454  pssnssi  45549  fourierdlem62  46612  fourierdlem68  46618  nthrucw  47332  abcdtb  47390  abcdtc  47391  abcdtd  47392  nabctnabc  47395  zlmodzxzsubm  48851  zlmodzxzldep  48996  ldepsnlinclem1  48997  ldepsnlinclem2  48998  sepfsepc  49419  idfth  49649  idsubc  49651  prstcleval  50046  prstcocval  50048  setc1onsubc  50093