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  8436  rdgdmlim  8457  oeoa  8635  oeoe  8637  ordtypelem3  9560  ordtypelem5  9562  ordtypelem6  9563  ordtypelem7  9564  ordtypelem9  9566  r1fin  9813  r1tr  9816  r1ordg  9818  r1ord3g  9819  r1pwss  9824  r1val1  9826  rankwflemb  9833  r1elwf  9836  rankr1ai  9838  rankdmr1  9841  rankr1ag  9842  rankr1bg  9843  pwwf  9847  unwf  9850  rankr1clem  9860  rankr1c  9861  rankval3b  9866  rankonidlem  9868  onssr1  9871  rankeq0b  9900  alephsuc2  10120  ackbij2  10282  wunom  10760  negiso  12248  infrenegsup  12251  om2uzoi  13996  faclbnd4lem1  14332  hashunlei  14464  hashsslei  14465  hashle2pr  14516  cos01bnd  16222  cos1bnd  16223  cos2bnd  16224  sincos2sgn  16230  sin4lt0  16231  egt2lt3  16242  divalglem9  16438  bitsinv  16485  drngui  20735  srasca  21183  cnfldfunALT  21379  cnfldfunALTOLD  21392  redvr  21635  refld  21637  iccpnfcnv  24975  xrhmph  24978  recvs  25179  recvsOLD  25180  qcvs  25181  i1f1  25725  itg11  25726  dvcos  26021  sinpi  26499  sinhalfpilem  26505  coshalfpi  26511  sincosq1lem  26539  tangtx  26547  sincos4thpi  26555  tan4thpi  26556  tan4thpiOLD  26557  sincos6thpi  26558  sincos3rdpi  26559  pige3ALT  26562  logltb  26642  1cubrlem  26884  1cubr  26885  log2tlbnd  26988  cxploglim2  27022  emcllem6  27044  emcllem7  27045  ppiublem1  27246  ppiublem2  27247  bposlem9  27336  lgsdir2lem4  27372  lgsdir2lem5  27373  chebbnd1lem2  27514  chebbnd1lem3  27515  chebbnd1  27516  dchrvmasumlema  27544  mulog2sumlem2  27579  pntlemb  27641  qdrng  27664  upgrbi  29110  upgr1elem  29129  usgrexmpledg  29279  ntrl2v2e  30177  frgrwopreg2  30338  normlem7tALT  31138  hhsssh  31288  shintcli  31348  chintcli  31350  omlsi  31423  qlaxr3i  31655  lnophm  32038  nmcopex  32048  nmcoplb  32049  nmbdfnlbi  32068  nmcfnex  32072  nmcfnlb  32073  hmopidmch  32172  hmopidmpj  32173  chirred  32414  1fldgenq  33324  zringfrac  33582  rrxdim  33665  constrextdg2  33790  2sqr3minply  33791  xrge0hmph  33931  qqh0  33985  qqh1  33986  rerrext  34010  zrhre  34020  qqhre  34021  mbfmvolf  34268  hgt750lem  34666  subfacval2  35192  erdszelem5  35200  erdszelem6  35201  erdszelem7  35202  erdszelem8  35203  filnetlem3  36381  filnetlem4  36382  bj-genr  36607  bj-genl  36608  bj-genan  36609  3lexlogpow5ineq5  42061  aks4d1p1p7  42075  tan3rdpi  42386  acos1half  42388  uun0.1  44798  pssnssi  45106  fourierdlem62  46183  fourierdlem68  46189  abcdtb  46938  abcdtc  46939  abcdtd  46940  nabctnabc  46943  zlmodzxzsubm  48275  zlmodzxzldep  48421  ldepsnlinclem1  48422  ldepsnlinclem2  48423  sepfsepc  48825  prstcleval  49157  prstcocval  49160