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  8367  rdgdmlim  8388  oeoa  8564  oeoe  8566  ordtypelem3  9480  ordtypelem5  9482  ordtypelem6  9483  ordtypelem7  9484  ordtypelem9  9486  r1fin  9733  r1tr  9736  r1ordg  9738  r1ord3g  9739  r1pwss  9744  r1val1  9746  rankwflemb  9753  r1elwf  9756  rankr1ai  9758  rankdmr1  9761  rankr1ag  9762  rankr1bg  9763  pwwf  9767  unwf  9770  rankr1clem  9780  rankr1c  9781  rankval3b  9786  rankonidlem  9788  onssr1  9791  rankeq0b  9820  alephsuc2  10040  ackbij2  10202  wunom  10680  negiso  12170  infrenegsup  12173  om2uzoi  13927  faclbnd4lem1  14265  hashunlei  14397  hashsslei  14398  hashle2pr  14449  cos01bnd  16161  cos1bnd  16162  cos2bnd  16163  sincos2sgn  16169  sin4lt0  16170  egt2lt3  16181  divalglem9  16378  bitsinv  16425  drngui  20651  srasca  21094  cnfldfunALT  21286  cnfldfunALTOLD  21299  redvr  21533  refld  21535  iccpnfcnv  24849  xrhmph  24852  recvs  25053  qcvs  25054  i1f1  25598  itg11  25599  dvcos  25894  sinpi  26372  sinhalfpilem  26379  coshalfpi  26385  sincosq1lem  26413  tangtx  26421  sincos4thpi  26429  tan4thpi  26430  tan4thpiOLD  26431  sincos6thpi  26432  sincos3rdpi  26433  pige3ALT  26436  logltb  26516  1cubrlem  26758  1cubr  26759  log2tlbnd  26862  cxploglim2  26896  emcllem6  26918  emcllem7  26919  ppiublem1  27120  ppiublem2  27121  bposlem9  27210  lgsdir2lem4  27246  lgsdir2lem5  27247  chebbnd1lem2  27388  chebbnd1lem3  27389  chebbnd1  27390  dchrvmasumlema  27418  mulog2sumlem2  27453  pntlemb  27515  qdrng  27538  upgrbi  29027  upgr1elem  29046  usgrexmpledg  29196  ntrl2v2e  30094  frgrwopreg2  30255  normlem7tALT  31055  hhsssh  31205  shintcli  31265  chintcli  31267  omlsi  31340  qlaxr3i  31572  lnophm  31955  nmcopex  31965  nmcoplb  31966  nmbdfnlbi  31985  nmcfnex  31989  nmcfnlb  31990  hmopidmch  32089  hmopidmpj  32090  chirred  32331  1fldgenq  33279  zringfrac  33532  rrxdim  33617  constrextdg2  33746  constrext2chnlem  33747  2sqr3minply  33777  2sqr3nconstr  33778  cos9thpiminply  33785  cos9thpinconstrlem2  33787  trisecnconstr  33789  xrge0hmph  33929  qqh0  33981  qqh1  33982  rerrext  34006  zrhre  34016  qqhre  34017  mbfmvolf  34264  hgt750lem  34649  subfacval2  35181  erdszelem5  35189  erdszelem6  35190  erdszelem7  35191  erdszelem8  35192  filnetlem3  36375  filnetlem4  36376  bj-genr  36601  bj-genl  36602  bj-genan  36603  3lexlogpow5ineq5  42055  aks4d1p1p7  42069  tan3rdpi  42347  cos2t3rdpi  42349  cos4t3rdpi  42351  acos1half  42353  uun0.1  44774  permaxpow  45006  pssnssi  45102  fourierdlem62  46173  fourierdlem68  46179  abcdtb  46931  abcdtc  46932  abcdtd  46933  nabctnabc  46936  zlmodzxzsubm  48351  zlmodzxzldep  48497  ldepsnlinclem1  48498  ldepsnlinclem2  48499  sepfsepc  48920  idfth  49151  idsubc  49153  prstcleval  49548  prstcocval  49550  setc1onsubc  49595