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  8408  rdgdmlim  8429  oeoa  8607  oeoe  8609  ordtypelem3  9532  ordtypelem5  9534  ordtypelem6  9535  ordtypelem7  9536  ordtypelem9  9538  r1fin  9785  r1tr  9788  r1ordg  9790  r1ord3g  9791  r1pwss  9796  r1val1  9798  rankwflemb  9805  r1elwf  9808  rankr1ai  9810  rankdmr1  9813  rankr1ag  9814  rankr1bg  9815  pwwf  9819  unwf  9822  rankr1clem  9832  rankr1c  9833  rankval3b  9838  rankonidlem  9840  onssr1  9843  rankeq0b  9872  alephsuc2  10092  ackbij2  10254  wunom  10732  negiso  12220  infrenegsup  12223  om2uzoi  13971  faclbnd4lem1  14309  hashunlei  14441  hashsslei  14442  hashle2pr  14493  cos01bnd  16202  cos1bnd  16203  cos2bnd  16204  sincos2sgn  16210  sin4lt0  16211  egt2lt3  16222  divalglem9  16418  bitsinv  16465  drngui  20693  srasca  21136  cnfldfunALT  21328  cnfldfunALTOLD  21341  redvr  21575  refld  21577  iccpnfcnv  24891  xrhmph  24894  recvs  25095  recvsOLD  25096  qcvs  25097  i1f1  25641  itg11  25642  dvcos  25937  sinpi  26415  sinhalfpilem  26422  coshalfpi  26428  sincosq1lem  26456  tangtx  26464  sincos4thpi  26472  tan4thpi  26473  tan4thpiOLD  26474  sincos6thpi  26475  sincos3rdpi  26476  pige3ALT  26479  logltb  26559  1cubrlem  26801  1cubr  26802  log2tlbnd  26905  cxploglim2  26939  emcllem6  26961  emcllem7  26962  ppiublem1  27163  ppiublem2  27164  bposlem9  27253  lgsdir2lem4  27289  lgsdir2lem5  27290  chebbnd1lem2  27431  chebbnd1lem3  27432  chebbnd1  27433  dchrvmasumlema  27461  mulog2sumlem2  27496  pntlemb  27558  qdrng  27581  upgrbi  29018  upgr1elem  29037  usgrexmpledg  29187  ntrl2v2e  30085  frgrwopreg2  30246  normlem7tALT  31046  hhsssh  31196  shintcli  31256  chintcli  31258  omlsi  31331  qlaxr3i  31563  lnophm  31946  nmcopex  31956  nmcoplb  31957  nmbdfnlbi  31976  nmcfnex  31980  nmcfnlb  31981  hmopidmch  32080  hmopidmpj  32081  chirred  32322  1fldgenq  33262  zringfrac  33515  rrxdim  33600  constrextdg2  33729  constrext2chnlem  33730  2sqr3minply  33760  2sqr3nconstr  33761  cos9thpiminply  33768  xrge0hmph  33909  qqh0  33961  qqh1  33962  rerrext  33986  zrhre  33996  qqhre  33997  mbfmvolf  34244  hgt750lem  34629  subfacval2  35155  erdszelem5  35163  erdszelem6  35164  erdszelem7  35165  erdszelem8  35166  filnetlem3  36344  filnetlem4  36345  bj-genr  36570  bj-genl  36571  bj-genan  36572  3lexlogpow5ineq5  42019  aks4d1p1p7  42033  tan3rdpi  42346  acos1half  42348  uun0.1  44750  permaxpow  44982  pssnssi  45073  fourierdlem62  46145  fourierdlem68  46151  abcdtb  46903  abcdtc  46904  abcdtd  46905  nabctnabc  46908  zlmodzxzsubm  48282  zlmodzxzldep  48428  ldepsnlinclem1  48429  ldepsnlinclem2  48430  sepfsepc  48850  idfth  49046  idsubc  49047  prstcleval  49380  prstcocval  49382  setc1onsubc  49427