Theorem simpri 487

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

Syntax hints:   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  tfr2b  8396  rdgdmlim  8417  oeoa  8597  oeoe  8599  ordtypelem3  9515  ordtypelem5  9517  ordtypelem6  9518  ordtypelem7  9519  ordtypelem9  9521  r1fin  9768  r1tr  9771  r1ordg  9773  r1ord3g  9774  r1pwss  9779  r1val1  9781  rankwflemb  9788  r1elwf  9791  rankr1ai  9793  rankdmr1  9796  rankr1ag  9797  rankr1bg  9798  pwwf  9802  unwf  9805  rankr1clem  9815  rankr1c  9816  rankval3b  9821  rankonidlem  9823  onssr1  9826  rankeq0b  9855  alephsuc2  10075  ackbij2  10238  wunom  10715  negiso  12194  infrenegsup  12197  om2uzoi  13920  faclbnd4lem1  14253  hashunlei  14385  hashsslei  14386  hashle2pr  14438  cos01bnd  16129  cos1bnd  16130  cos2bnd  16131  sincos2sgn  16137  sin4lt0  16138  egt2lt3  16149  divalglem9  16344  bitsinv  16389  drngui  20363  srasca  20798  cnfldfunALT  20957  redvr  21170  refld  21172  iccpnfcnv  24460  xrhmph  24463  recvs  24662  recvsOLD  24663  qcvs  24664  i1f1  25207  itg11  25208  dvcos  25500  sinpi  25967  sinhalfpilem  25973  coshalfpi  25979  sincosq1lem  26007  tangtx  26015  sincos4thpi  26023  tan4thpi  26024  sincos6thpi  26025  sincos3rdpi  26026  pige3ALT  26029  logltb  26108  1cubrlem  26346  1cubr  26347  log2tlbnd  26450  cxploglim2  26483  emcllem6  26505  emcllem7  26506  ppiublem1  26705  ppiublem2  26706  bposlem9  26795  lgsdir2lem4  26831  lgsdir2lem5  26832  chebbnd1lem2  26973  chebbnd1lem3  26974  chebbnd1  26975  dchrvmasumlema  27003  mulog2sumlem2  27038  pntlemb  27100  qdrng  27123  upgrbi  28353  upgr1elem  28372  usgrexmpledg  28519  ntrl2v2e  29411  frgrwopreg2  29572  normlem7tALT  30372  hhsssh  30522  shintcli  30582  chintcli  30584  omlsi  30657  qlaxr3i  30889  lnophm  31272  nmcopex  31282  nmcoplb  31283  nmbdfnlbi  31302  nmcfnex  31306  nmcfnlb  31307  hmopidmch  31406  hmopidmpj  31407  chirred  31648  1fldgenq  32412  rrxdim  32699  xrge0hmph  32912  qqh0  32964  qqh1  32965  rerrext  32989  zrhre  32999  qqhre  33000  mbfmvolf  33265  hgt750lem  33663  subfacval2  34178  erdszelem5  34186  erdszelem6  34187  erdszelem7  34188  erdszelem8  34189  filnetlem3  35265  filnetlem4  35266  bj-genr  35484  bj-genl  35485  bj-genan  35486  3lexlogpow5ineq5  40925  aks4d1p1p7  40939  acos1half  41415  uun0.1  43539  pssnssi  43790  fourierdlem62  44884  fourierdlem68  44890  abcdtb  45636  abcdtc  45637  abcdtd  45638  nabctnabc  45641  zlmodzxzsubm  47035  zlmodzxzldep  47185  ldepsnlinclem1  47186  ldepsnlinclem2  47187  sepfsepc  47560  prstcleval  47688  prstcocval  47691