Theorem simpri 490

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

Syntax hints:   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  tfr2b  8382  rdgdmlim  8403  oeoa  8582  oeoe  8584  ordtypelem3  9481  ordtypelem5  9483  ordtypelem6  9484  ordtypelem7  9485  ordtypelem9  9487  r1fin  9744  r1tr  9747  r1ordg  9749  r1ord3g  9750  r1pwss  9755  r1val1  9757  rankwflemb  9764  r1elwf  9767  rankr1ai  9769  rankdmr1  9772  rankr1ag  9773  rankr1bg  9774  pwwf  9778  unwf  9781  rankr1clem  9791  rankr1c  9792  rankval3b  9797  rankonidlem  9799  onssr1  9802  rankeq0b  9831  alephsuc2  10063  ackbij2  10224  wunom  10704  negiso  12194  infrenegsup  12197  om2uzoi  13991  faclbnd4lem1  14329  hashunlei  14462  hashsslei  14463  hashle2pr  14514  cos01bnd  16241  cos1bnd  16242  cos2bnd  16243  sincos2sgn  16249  sin4lt0  16250  egt2lt3  16261  divalglem9  16458  bitsinv  16505  drngui  20818  srasca  21280  cnfldfunALT  21516  redvr  21746  refld  21748  iccpnfcnv  25082  xrhmph  25085  recvs  25284  qcvs  25285  i1f1  25828  itg11  25829  dvcos  26121  sinpi  26594  sinhalfpilem  26604  coshalfpi  26610  sincosq1lem  26638  tangtx  26646  sincos4thpi  26654  tan4thpi  26655  tan4thpiOLD  26656  sincos6thpi  26657  sincos3rdpi  26658  pige3ALT  26661  logltb  26741  1cubrlem  26982  1cubr  26983  log2tlbnd  27086  cxploglim2  27119  emcllem6  27141  emcllem7  27142  ppiublem1  27342  ppiublem2  27343  bposlem9  27432  lgsdir2lem4  27468  lgsdir2lem5  27469  chebbnd1lem2  27610  chebbnd1lem3  27611  chebbnd1  27612  dchrvmasumlema  27640  mulog2sumlem2  27675  pntlemb  27737  qdrng  27760  upgrbi  29409  upgr1elem  29428  usgrexmpledg  29578  ntrl2v2e  30475  frgrwopreg2  30636  normlem7tALT  31437  hhsssh  31587  shintcli  31647  chintcli  31649  omlsi  31722  qlaxr3i  31954  lnophm  32337  nmcopex  32347  nmcoplb  32348  nmbdfnlbi  32367  nmcfnex  32371  nmcfnlb  32372  hmopidmch  32471  hmopidmpj  32472  chirred  32713  1fldgenq  33609  zringfrac  33810  esplyind  33931  rrxdim  33970  constrextdg2  34105  constrext2chnlem  34106  2sqr3minply  34136  2sqr3nconstr  34137  cos9thpiminply  34144  cos9thpinconstrlem2  34146  trisecnconstr  34148  xrge0hmph  34288  qqh0  34340  qqh1  34341  rerrext  34365  zrhre  34375  qqhre  34376  mbfmvolf  34622  hgt750lem  35004  r11  35453  r12  35454  subfacval2  35645  erdszelem5  35653  erdszelem6  35654  erdszelem7  35655  erdszelem8  35656  filnetlem3  36857  filnetlem4  36858  bj-genr  37166  bj-genl  37167  bj-genan  37168  3lexlogpow5ineq5  42795  aks4d1p1p7  42809  tan3rdpi  43081  cos2t3rdpi  43083  cos4t3rdpi  43085  acos1half  43087  uun0.1  45456  permaxpow  45688  pssnssi  45789  fourierdlem62  46852  fourierdlem68  46858  nthrucw  47572  abcdtb  47630  abcdtc  47631  abcdtd  47632  nabctnabc  47635  zlmodzxzsubm  49106  zlmodzxzldep  49251  ldepsnlinclem1  49252  ldepsnlinclem2  49253  sepfsepc  49673  idfth  49903  idsubc  49905  prstcleval  50300  prstcocval  50302  setc1onsubc  50347