Theorem simpri 485

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

Syntax hints:   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  tfr2b  8364  rdgdmlim  8385  oeoa  8561  oeoe  8563  ordtypelem3  9473  ordtypelem5  9475  ordtypelem6  9476  ordtypelem7  9477  ordtypelem9  9479  r1fin  9726  r1tr  9729  r1ordg  9731  r1ord3g  9732  r1pwss  9737  r1val1  9739  rankwflemb  9746  r1elwf  9749  rankr1ai  9751  rankdmr1  9754  rankr1ag  9755  rankr1bg  9756  pwwf  9760  unwf  9763  rankr1clem  9773  rankr1c  9774  rankval3b  9779  rankonidlem  9781  onssr1  9784  rankeq0b  9813  alephsuc2  10033  ackbij2  10195  wunom  10673  negiso  12163  infrenegsup  12166  om2uzoi  13920  faclbnd4lem1  14258  hashunlei  14390  hashsslei  14391  hashle2pr  14442  cos01bnd  16154  cos1bnd  16155  cos2bnd  16156  sincos2sgn  16162  sin4lt0  16163  egt2lt3  16174  divalglem9  16371  bitsinv  16418  drngui  20644  srasca  21087  cnfldfunALT  21279  cnfldfunALTOLD  21292  redvr  21526  refld  21528  iccpnfcnv  24842  xrhmph  24845  recvs  25046  qcvs  25047  i1f1  25591  itg11  25592  dvcos  25887  sinpi  26365  sinhalfpilem  26372  coshalfpi  26378  sincosq1lem  26406  tangtx  26414  sincos4thpi  26422  tan4thpi  26423  tan4thpiOLD  26424  sincos6thpi  26425  sincos3rdpi  26426  pige3ALT  26429  logltb  26509  1cubrlem  26751  1cubr  26752  log2tlbnd  26855  cxploglim2  26889  emcllem6  26911  emcllem7  26912  ppiublem1  27113  ppiublem2  27114  bposlem9  27203  lgsdir2lem4  27239  lgsdir2lem5  27240  chebbnd1lem2  27381  chebbnd1lem3  27382  chebbnd1  27383  dchrvmasumlema  27411  mulog2sumlem2  27446  pntlemb  27508  qdrng  27531  upgrbi  29020  upgr1elem  29039  usgrexmpledg  29189  ntrl2v2e  30087  frgrwopreg2  30248  normlem7tALT  31048  hhsssh  31198  shintcli  31258  chintcli  31260  omlsi  31333  qlaxr3i  31565  lnophm  31948  nmcopex  31958  nmcoplb  31959  nmbdfnlbi  31978  nmcfnex  31982  nmcfnlb  31983  hmopidmch  32082  hmopidmpj  32083  chirred  32324  1fldgenq  33272  zringfrac  33525  rrxdim  33610  constrextdg2  33739  constrext2chnlem  33740  2sqr3minply  33770  2sqr3nconstr  33771  cos9thpiminply  33778  cos9thpinconstrlem2  33780  trisecnconstr  33782  xrge0hmph  33922  qqh0  33974  qqh1  33975  rerrext  33999  zrhre  34009  qqhre  34010  mbfmvolf  34257  hgt750lem  34642  subfacval2  35174  erdszelem5  35182  erdszelem6  35183  erdszelem7  35184  erdszelem8  35185  filnetlem3  36368  filnetlem4  36369  bj-genr  36594  bj-genl  36595  bj-genan  36596  3lexlogpow5ineq5  42048  aks4d1p1p7  42062  tan3rdpi  42340  cos2t3rdpi  42342  cos4t3rdpi  42344  acos1half  42346  uun0.1  44767  permaxpow  44999  pssnssi  45095  fourierdlem62  46166  fourierdlem68  46172  abcdtb  46927  abcdtc  46928  abcdtd  46929  nabctnabc  46932  zlmodzxzsubm  48347  zlmodzxzldep  48493  ldepsnlinclem1  48494  ldepsnlinclem2  48495  sepfsepc  48916  idfth  49147  idsubc  49149  prstcleval  49544  prstcocval  49546  setc1onsubc  49591