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  8325  rdgdmlim  8346  oeoa  8522  oeoe  8524  ordtypelem3  9431  ordtypelem5  9433  ordtypelem6  9434  ordtypelem7  9435  ordtypelem9  9437  r1fin  9688  r1tr  9691  r1ordg  9693  r1ord3g  9694  r1pwss  9699  r1val1  9701  rankwflemb  9708  r1elwf  9711  rankr1ai  9713  rankdmr1  9716  rankr1ag  9717  rankr1bg  9718  pwwf  9722  unwf  9725  rankr1clem  9735  rankr1c  9736  rankval3b  9741  rankonidlem  9743  onssr1  9746  rankeq0b  9775  alephsuc2  9993  ackbij2  10155  wunom  10633  negiso  12123  infrenegsup  12126  om2uzoi  13880  faclbnd4lem1  14218  hashunlei  14350  hashsslei  14351  hashle2pr  14402  cos01bnd  16113  cos1bnd  16114  cos2bnd  16115  sincos2sgn  16121  sin4lt0  16122  egt2lt3  16133  divalglem9  16330  bitsinv  16377  drngui  20638  srasca  21102  cnfldfunALT  21294  cnfldfunALTOLD  21307  redvr  21542  refld  21544  iccpnfcnv  24858  xrhmph  24861  recvs  25062  qcvs  25063  i1f1  25607  itg11  25608  dvcos  25903  sinpi  26381  sinhalfpilem  26388  coshalfpi  26394  sincosq1lem  26422  tangtx  26430  sincos4thpi  26438  tan4thpi  26439  tan4thpiOLD  26440  sincos6thpi  26441  sincos3rdpi  26442  pige3ALT  26445  logltb  26525  1cubrlem  26767  1cubr  26768  log2tlbnd  26871  cxploglim2  26905  emcllem6  26927  emcllem7  26928  ppiublem1  27129  ppiublem2  27130  bposlem9  27219  lgsdir2lem4  27255  lgsdir2lem5  27256  chebbnd1lem2  27397  chebbnd1lem3  27398  chebbnd1  27399  dchrvmasumlema  27427  mulog2sumlem2  27462  pntlemb  27524  qdrng  27547  upgrbi  29056  upgr1elem  29075  usgrexmpledg  29225  ntrl2v2e  30120  frgrwopreg2  30281  normlem7tALT  31081  hhsssh  31231  shintcli  31291  chintcli  31293  omlsi  31366  qlaxr3i  31598  lnophm  31981  nmcopex  31991  nmcoplb  31992  nmbdfnlbi  32011  nmcfnex  32015  nmcfnlb  32016  hmopidmch  32115  hmopidmpj  32116  chirred  32357  1fldgenq  33271  zringfrac  33501  rrxdim  33586  constrextdg2  33715  constrext2chnlem  33716  2sqr3minply  33746  2sqr3nconstr  33747  cos9thpiminply  33754  cos9thpinconstrlem2  33756  trisecnconstr  33758  xrge0hmph  33898  qqh0  33950  qqh1  33951  rerrext  33975  zrhre  33985  qqhre  33986  mbfmvolf  34233  hgt750lem  34618  subfacval2  35159  erdszelem5  35167  erdszelem6  35168  erdszelem7  35169  erdszelem8  35170  filnetlem3  36353  filnetlem4  36354  bj-genr  36579  bj-genl  36580  bj-genan  36581  3lexlogpow5ineq5  42033  aks4d1p1p7  42047  tan3rdpi  42325  cos2t3rdpi  42327  cos4t3rdpi  42329  acos1half  42331  uun0.1  44751  permaxpow  44983  pssnssi  45079  fourierdlem62  46150  fourierdlem68  46156  abcdtb  46911  abcdtc  46912  abcdtd  46913  nabctnabc  46916  zlmodzxzsubm  48331  zlmodzxzldep  48477  ldepsnlinclem1  48478  ldepsnlinclem2  48479  sepfsepc  48900  idfth  49131  idsubc  49133  prstcleval  49528  prstcocval  49530  setc1onsubc  49575