Theorem simpri 488

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

Syntax hints:   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  tfr2b  8355  rdgdmlim  8376  oeoa  8555  oeoe  8557  ordtypelem3  9458  ordtypelem5  9460  ordtypelem6  9461  ordtypelem7  9462  ordtypelem9  9464  r1fin  9721  r1tr  9724  r1ordg  9726  r1ord3g  9727  r1pwss  9732  r1val1  9734  rankwflemb  9741  r1elwf  9744  rankr1ai  9746  rankdmr1  9749  rankr1ag  9750  rankr1bg  9751  pwwf  9755  unwf  9758  rankr1clem  9768  rankr1c  9769  rankval3b  9774  rankonidlem  9776  onssr1  9779  rankeq0b  9808  alephsuc2  10026  ackbij2  10188  wunom  10668  negiso  12162  infrenegsup  12165  om2uzoi  13958  faclbnd4lem1  14296  hashunlei  14428  hashsslei  14429  hashle2pr  14480  cos01bnd  16194  cos1bnd  16195  cos2bnd  16196  sincos2sgn  16202  sin4lt0  16203  egt2lt3  16214  divalglem9  16411  bitsinv  16458  drngui  20757  srasca  21220  cnfldfunALT  21412  redvr  21642  refld  21644  iccpnfcnv  24979  xrhmph  24982  recvs  25181  qcvs  25182  i1f1  25725  itg11  25726  dvcos  26018  sinpi  26488  sinhalfpilem  26498  coshalfpi  26504  sincosq1lem  26532  tangtx  26540  sincos4thpi  26548  tan4thpi  26549  tan4thpiOLD  26550  sincos6thpi  26551  sincos3rdpi  26552  pige3ALT  26555  logltb  26635  1cubrlem  26876  1cubr  26877  log2tlbnd  26980  cxploglim2  27013  emcllem6  27035  emcllem7  27036  ppiublem1  27236  ppiublem2  27237  bposlem9  27326  lgsdir2lem4  27362  lgsdir2lem5  27363  chebbnd1lem2  27504  chebbnd1lem3  27505  chebbnd1  27506  dchrvmasumlema  27534  mulog2sumlem2  27569  pntlemb  27631  qdrng  27654  upgrbi  29233  upgr1elem  29252  usgrexmpledg  29402  ntrl2v2e  30299  frgrwopreg2  30460  normlem7tALT  31261  hhsssh  31411  shintcli  31471  chintcli  31473  omlsi  31546  qlaxr3i  31778  lnophm  32161  nmcopex  32171  nmcoplb  32172  nmbdfnlbi  32191  nmcfnex  32195  nmcfnlb  32196  hmopidmch  32295  hmopidmpj  32296  chirred  32537  1fldgenq  33463  zringfrac  33704  esplyind  33826  rrxdim  33865  constrextdg2  34000  constrext2chnlem  34001  2sqr3minply  34031  2sqr3nconstr  34032  cos9thpiminply  34039  cos9thpinconstrlem2  34041  trisecnconstr  34043  xrge0hmph  34183  qqh0  34235  qqh1  34236  rerrext  34260  zrhre  34270  qqhre  34271  mbfmvolf  34517  hgt750lem  34902  r11  35345  r12  35346  subfacval2  35485  erdszelem5  35493  erdszelem6  35494  erdszelem7  35495  erdszelem8  35496  filnetlem3  36688  filnetlem4  36689  bj-genr  36998  bj-genl  36999  bj-genan  37000  3lexlogpow5ineq5  42625  aks4d1p1p7  42639  tan3rdpi  42909  cos2t3rdpi  42911  cos4t3rdpi  42913  acos1half  42915  uun0.1  45301  permaxpow  45533  pssnssi  45627  fourierdlem62  46690  fourierdlem68  46696  nthrucw  47410  abcdtb  47468  abcdtc  47469  abcdtd  47470  nabctnabc  47473  zlmodzxzsubm  48929  zlmodzxzldep  49074  ldepsnlinclem1  49075  ldepsnlinclem2  49076  sepfsepc  49497  idfth  49727  idsubc  49729  prstcleval  50124  prstcocval  50126  setc1onsubc  50171