Theorem simpri 491

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

This proof depends on syntax axioms:   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  tfr2b  8432  rdgdmlim  8453  oeoa  8634  oeoe  8636  ordtypelem3  9541  ordtypelem5  9543  ordtypelem6  9544  ordtypelem7  9545  ordtypelem9  9547  alephsuc2  10186  negiso  12324  infrenegsup  12327  om2uzoi  14125  faclbnd4lem1  14464  hashunlei  14597  hashsslei  14598  hashle2pr  14649  cos01bnd  16383  cos1bnd  16384  cos2bnd  16385  sincos2sgn  16391  sin4lt0  16392  egt2lt3  16403  divalglem9  16600  bitsinv  16647  drngui  21016  srasca  21485  cnfldfunALT  21723  redvr  21953  refld  21955  iccpnfcnv  25295  xrhmph  25298  recvs  25497  qcvs  25498  i1f1  26041  itg11  26042  dvcos  26333  sinpi  26812  sinhalfpilem  26822  coshalfpi  26828  sincosq1lem  26856  tangtx  26864  sincos4thpi  26872  tan4thpi  26873  sincos6thpi  26874  sincos3rdpi  26875  pige3ALT  26878  logltb  26958  1cubrlem  27199  1cubr  27200  log2tlbnd  27303  cxploglim2  27336  emcllem6  27358  emcllem7  27359  ppiublem1  27559  ppiublem2  27560  bposlem9  27649  lgsdir2lem4  27685  lgsdir2lem5  27686  chebbnd1lem2  27827  chebbnd1lem3  27828  chebbnd1  27829  dchrvmasumlema  27857  mulog2sumlem2  27892  pntlemb  27954  qdrng  27977  upgrbi  29701  upgr1elem  29720  usgrexmpledg  29873  ntrl2v2e  30789  frgrwopreg2  30950  normlem7tALT  31751  hhsssh  31901  shintcli  31961  chintcli  31963  omlsi  32036  qlaxr3i  32268  lnophm  32651  nmcopex  32661  nmcoplb  32662  nmbdfnlbi  32681  nmcfnex  32685  nmcfnlb  32686  hmopidmch  32785  hmopidmpj  32786  chirred  33027  1fldgenq  33954  zringfrac  34156  esplyind  34277  rrxdim  34316  constrextdg2  34451  constrext2chnlem  34452  2sqr3minply  34482  2sqr3nconstr  34483  cos9thpiminply  34490  cos9thpinconstrlem2  34492  trisecnconstr  34494  xrge0hmph  34634  qqh0  34686  qqh1  34687  rerrext  34711  zrhre  34721  qqhre  34722  mbfmvolf  34968  hgt750lem  35350  gdlopcfvlem  35971  subfacval2  36119  erdszelem5  36127  erdszelem6  36128  erdszelem7  36129  erdszelem8  36130  filnetlem3  37346  filnetlem4  37347  bj-genr  37655  bj-genl  37656  bj-genan  37657  3lexlogpow5ineq5  43302  aks4d1p1p7  43316  tan3rdpi  43596  cos2t3rdpi  43598  cos4t3rdpi  43600  acos1half  43602  uun0.1  45951  permaxpow  46194  hfstructhf  46228  hfstructcan  46229  pssnssi  46321  fourierdlem62  47383  fourierdlem68  47389  numtowerdt  48121  abcdtb  48201  abcdtc  48202  abcdtd  48203  nabctnabc  48206  zlmodzxzsubm  49676  zlmodzxzldep  49821  ldepsnlinclem1  49822  ldepsnlinclem2  49823  sepfsepc  50247  idfth  50479  idsubc  50481  prstcleval  50898  prstcocval  50900  setc1onsubc  50945  fuconuniqlem  50986  fuconuniqvalslem  50988  veroquaddetzerod  51266