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:  exanOLD  1863  tfr2b  8034  rdgdmlim  8055  oeoa  8225  oeoe  8227  ordtypelem3  8986  ordtypelem5  8988  ordtypelem6  8989  ordtypelem7  8990  ordtypelem9  8992  r1fin  9204  r1tr  9207  r1ordg  9209  r1ord3g  9210  r1pwss  9215  r1val1  9217  rankwflemb  9224  r1elwf  9227  rankr1ai  9229  rankdmr1  9232  rankr1ag  9233  rankr1bg  9234  pwwf  9238  unwf  9241  rankr1clem  9251  rankr1c  9252  rankval3b  9257  rankonidlem  9259  onssr1  9262  rankeq0b  9291  alephsuc2  9508  ackbij2  9667  wunom  10144  negiso  11623  infrenegsup  11626  om2uzoi  13326  faclbnd4lem1  13656  hashunlei  13789  hashsslei  13790  hashle2pr  13838  cos01bnd  15541  cos1bnd  15542  cos2bnd  15543  sincos2sgn  15549  sin4lt0  15550  egt2lt3  15561  divalglem9  15754  bitsinv  15799  drngui  19510  redvr  20763  refld  20765  recrng  20767  iccpnfcnv  23550  xrhmph  23553  recvs  23752  qcvs  23753  i1f1  24293  itg11  24294  dvcos  24582  sinpi  25045  sinhalfpilem  25051  coshalfpi  25057  sincosq1lem  25085  tangtx  25093  sincos4thpi  25101  tan4thpi  25102  sincos6thpi  25103  sincos3rdpi  25104  pige3ALT  25107  logltb  25185  1cubrlem  25421  1cubr  25422  log2tlbnd  25525  cxploglim2  25558  emcllem6  25580  emcllem7  25581  ppiublem1  25780  ppiublem2  25781  bposlem9  25870  lgsdir2lem4  25906  lgsdir2lem5  25907  chebbnd1lem2  26048  chebbnd1lem3  26049  chebbnd1  26050  dchrvmasumlema  26078  mulog2sumlem2  26113  pntlemb  26175  qdrng  26198  upgrbi  26880  upgr1elem  26899  usgrexmpledg  27046  ntrl2v2e  27939  frgrwopreg2  28100  normlem7tALT  28898  hhsssh  29048  shintcli  29108  chintcli  29110  omlsi  29183  qlaxr3i  29415  lnophm  29798  nmcopex  29808  nmcoplb  29809  nmbdfnlbi  29828  nmcfnex  29832  nmcfnlb  29833  hmopidmch  29932  hmopidmpj  29933  chirred  30174  rrxdim  31014  xrge0hmph  31177  qqh0  31227  qqh1  31228  rerrext  31252  zrhre  31262  qqhre  31263  mbfmvolf  31526  hgt750lem  31924  subfacval2  32436  erdszelem5  32444  erdszelem6  32445  erdszelem7  32446  erdszelem8  32447  filnetlem3  33730  filnetlem4  33731  bj-genr  33942  bj-genl  33943  bj-genan  33944  uun0.1  41119  pssnssi  41374  fourierdlem62  42460  fourierdlem68  42466  abcdtb  43169  abcdtc  43170  abcdtd  43171  nabctnabc  43174  zlmodzxzsubm  44414  zlmodzxzldep  44566  ldepsnlinclem1  44567  ldepsnlinclem2  44568