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  8335  rdgdmlim  8356  oeoa  8533  oeoe  8535  ordtypelem3  9435  ordtypelem5  9437  ordtypelem6  9438  ordtypelem7  9439  ordtypelem9  9441  r1fin  9697  r1tr  9700  r1ordg  9702  r1ord3g  9703  r1pwss  9708  r1val1  9710  rankwflemb  9717  r1elwf  9720  rankr1ai  9722  rankdmr1  9725  rankr1ag  9726  rankr1bg  9727  pwwf  9731  unwf  9734  rankr1clem  9744  rankr1c  9745  rankval3b  9750  rankonidlem  9752  onssr1  9755  rankeq0b  9784  alephsuc2  10002  ackbij2  10164  wunom  10643  negiso  12136  infrenegsup  12139  om2uzoi  13917  faclbnd4lem1  14255  hashunlei  14387  hashsslei  14388  hashle2pr  14439  cos01bnd  16153  cos1bnd  16154  cos2bnd  16155  sincos2sgn  16161  sin4lt0  16162  egt2lt3  16173  divalglem9  16370  bitsinv  16417  drngui  20712  srasca  21175  cnfldfunALT  21367  redvr  21597  refld  21599  iccpnfcnv  24911  xrhmph  24914  recvs  25113  qcvs  25114  i1f1  25657  itg11  25658  dvcos  25950  sinpi  26420  sinhalfpilem  26427  coshalfpi  26433  sincosq1lem  26461  tangtx  26469  sincos4thpi  26477  tan4thpi  26478  tan4thpiOLD  26479  sincos6thpi  26480  sincos3rdpi  26481  pige3ALT  26484  logltb  26564  1cubrlem  26805  1cubr  26806  log2tlbnd  26909  cxploglim2  26942  emcllem6  26964  emcllem7  26965  ppiublem1  27165  ppiublem2  27166  bposlem9  27255  lgsdir2lem4  27291  lgsdir2lem5  27292  chebbnd1lem2  27433  chebbnd1lem3  27434  chebbnd1  27435  dchrvmasumlema  27463  mulog2sumlem2  27498  pntlemb  27560  qdrng  27583  upgrbi  29162  upgr1elem  29181  usgrexmpledg  29331  ntrl2v2e  30228  frgrwopreg2  30389  normlem7tALT  31190  hhsssh  31340  shintcli  31400  chintcli  31402  omlsi  31475  qlaxr3i  31707  lnophm  32090  nmcopex  32100  nmcoplb  32101  nmbdfnlbi  32120  nmcfnex  32124  nmcfnlb  32125  hmopidmch  32224  hmopidmpj  32225  chirred  32466  1fldgenq  33383  zringfrac  33614  esplyind  33719  rrxdim  33758  constrextdg2  33893  constrext2chnlem  33894  2sqr3minply  33924  2sqr3nconstr  33925  cos9thpiminply  33932  cos9thpinconstrlem2  33934  trisecnconstr  33936  xrge0hmph  34076  qqh0  34128  qqh1  34129  rerrext  34153  zrhre  34163  qqhre  34164  mbfmvolf  34410  hgt750lem  34795  r11  35237  r12  35238  subfacval2  35369  erdszelem5  35377  erdszelem6  35378  erdszelem7  35379  erdszelem8  35380  filnetlem3  36562  filnetlem4  36563  bj-genr  36872  bj-genl  36873  bj-genan  36874  3lexlogpow5ineq5  42499  aks4d1p1p7  42513  tan3rdpi  42784  cos2t3rdpi  42786  cos4t3rdpi  42788  acos1half  42790  uun0.1  45204  permaxpow  45436  pssnssi  45531  fourierdlem62  46596  fourierdlem68  46602  nthrucw  47314  abcdtb  47368  abcdtc  47369  abcdtd  47370  nabctnabc  47373  zlmodzxzsubm  48829  zlmodzxzldep  48974  ldepsnlinclem1  48975  ldepsnlinclem2  48976  sepfsepc  49397  idfth  49627  idsubc  49629  prstcleval  50024  prstcocval  50026  setc1onsubc  50071