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  8337  rdgdmlim  8358  oeoa  8535  oeoe  8537  ordtypelem3  9437  ordtypelem5  9439  ordtypelem6  9440  ordtypelem7  9441  ordtypelem9  9443  r1fin  9697  r1tr  9700  r1ordg  9702  r1ord3g  9703  r1pwss  9708  r1val1  9710  rankwflemb  9717  r1elwf  9720  rankr1ai  9722  rankdmr1  9725  rankr1ag  9726  rankr1bg  9727  pwwf  9731  unwf  9734  rankr1clem  9744  rankr1c  9745  rankval3b  9750  rankonidlem  9752  onssr1  9755  rankeq0b  9784  alephsuc2  10002  ackbij2  10164  wunom  10643  negiso  12134  infrenegsup  12137  om2uzoi  13890  faclbnd4lem1  14228  hashunlei  14360  hashsslei  14361  hashle2pr  14412  cos01bnd  16123  cos1bnd  16124  cos2bnd  16125  sincos2sgn  16131  sin4lt0  16132  egt2lt3  16143  divalglem9  16340  bitsinv  16387  drngui  20680  srasca  21144  cnfldfunALT  21336  cnfldfunALTOLD  21349  redvr  21584  refld  21586  iccpnfcnv  24910  xrhmph  24913  recvs  25114  qcvs  25115  i1f1  25659  itg11  25660  dvcos  25955  sinpi  26433  sinhalfpilem  26440  coshalfpi  26446  sincosq1lem  26474  tangtx  26482  sincos4thpi  26490  tan4thpi  26491  tan4thpiOLD  26492  sincos6thpi  26493  sincos3rdpi  26494  pige3ALT  26497  logltb  26577  1cubrlem  26819  1cubr  26820  log2tlbnd  26923  cxploglim2  26957  emcllem6  26979  emcllem7  26980  ppiublem1  27181  ppiublem2  27182  bposlem9  27271  lgsdir2lem4  27307  lgsdir2lem5  27308  chebbnd1lem2  27449  chebbnd1lem3  27450  chebbnd1  27451  dchrvmasumlema  27479  mulog2sumlem2  27514  pntlemb  27576  qdrng  27599  upgrbi  29178  upgr1elem  29197  usgrexmpledg  29347  ntrl2v2e  30245  frgrwopreg2  30406  normlem7tALT  31206  hhsssh  31356  shintcli  31416  chintcli  31418  omlsi  31491  qlaxr3i  31723  lnophm  32106  nmcopex  32116  nmcoplb  32117  nmbdfnlbi  32136  nmcfnex  32140  nmcfnlb  32141  hmopidmch  32240  hmopidmpj  32241  chirred  32482  1fldgenq  33415  zringfrac  33646  esplyind  33751  rrxdim  33791  constrextdg2  33926  constrext2chnlem  33927  2sqr3minply  33957  2sqr3nconstr  33958  cos9thpiminply  33965  cos9thpinconstrlem2  33967  trisecnconstr  33969  xrge0hmph  34109  qqh0  34161  qqh1  34162  rerrext  34186  zrhre  34196  qqhre  34197  mbfmvolf  34443  hgt750lem  34828  r11  35269  r12  35270  subfacval2  35400  erdszelem5  35408  erdszelem6  35409  erdszelem7  35410  erdszelem8  35411  filnetlem3  36593  filnetlem4  36594  bj-genr  36827  bj-genl  36828  bj-genan  36829  3lexlogpow5ineq5  42419  aks4d1p1p7  42433  tan3rdpi  42711  cos2t3rdpi  42713  cos4t3rdpi  42715  acos1half  42717  uun0.1  45122  permaxpow  45354  pssnssi  45449  fourierdlem62  46515  fourierdlem68  46521  nthrucw  47233  abcdtb  47275  abcdtc  47276  abcdtd  47277  nabctnabc  47280  zlmodzxzsubm  48708  zlmodzxzldep  48853  ldepsnlinclem1  48854  ldepsnlinclem2  48855  sepfsepc  49276  idfth  49506  idsubc  49508  prstcleval  49903  prstcocval  49905  setc1onsubc  49950