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  8326  rdgdmlim  8347  oeoa  8524  oeoe  8526  ordtypelem3  9426  ordtypelem5  9428  ordtypelem6  9429  ordtypelem7  9430  ordtypelem9  9432  r1fin  9686  r1tr  9689  r1ordg  9691  r1ord3g  9692  r1pwss  9697  r1val1  9699  rankwflemb  9706  r1elwf  9709  rankr1ai  9711  rankdmr1  9714  rankr1ag  9715  rankr1bg  9716  pwwf  9720  unwf  9723  rankr1clem  9733  rankr1c  9734  rankval3b  9739  rankonidlem  9741  onssr1  9744  rankeq0b  9773  alephsuc2  9991  ackbij2  10153  wunom  10632  negiso  12125  infrenegsup  12128  om2uzoi  13906  faclbnd4lem1  14244  hashunlei  14376  hashsslei  14377  hashle2pr  14428  cos01bnd  16142  cos1bnd  16143  cos2bnd  16144  sincos2sgn  16150  sin4lt0  16151  egt2lt3  16162  divalglem9  16359  bitsinv  16406  drngui  20701  srasca  21165  cnfldfunALT  21357  cnfldfunALTOLD  21370  redvr  21605  refld  21607  iccpnfcnv  24920  xrhmph  24923  recvs  25122  qcvs  25123  i1f1  25666  itg11  25667  dvcos  25959  sinpi  26436  sinhalfpilem  26443  coshalfpi  26449  sincosq1lem  26477  tangtx  26485  sincos4thpi  26493  tan4thpi  26494  tan4thpiOLD  26495  sincos6thpi  26496  sincos3rdpi  26497  pige3ALT  26500  logltb  26580  1cubrlem  26822  1cubr  26823  log2tlbnd  26926  cxploglim2  26960  emcllem6  26982  emcllem7  26983  ppiublem1  27184  ppiublem2  27185  bposlem9  27274  lgsdir2lem4  27310  lgsdir2lem5  27311  chebbnd1lem2  27452  chebbnd1lem3  27453  chebbnd1  27454  dchrvmasumlema  27482  mulog2sumlem2  27517  pntlemb  27579  qdrng  27602  upgrbi  29181  upgr1elem  29200  usgrexmpledg  29350  ntrl2v2e  30248  frgrwopreg2  30409  normlem7tALT  31210  hhsssh  31360  shintcli  31420  chintcli  31422  omlsi  31495  qlaxr3i  31727  lnophm  32110  nmcopex  32120  nmcoplb  32121  nmbdfnlbi  32140  nmcfnex  32144  nmcfnlb  32145  hmopidmch  32244  hmopidmpj  32245  chirred  32486  1fldgenq  33403  zringfrac  33634  esplyind  33739  rrxdim  33779  constrextdg2  33914  constrext2chnlem  33915  2sqr3minply  33945  2sqr3nconstr  33946  cos9thpiminply  33953  cos9thpinconstrlem2  33955  trisecnconstr  33957  xrge0hmph  34097  qqh0  34149  qqh1  34150  rerrext  34174  zrhre  34184  qqhre  34185  mbfmvolf  34431  hgt750lem  34816  r11  35258  r12  35259  subfacval2  35390  erdszelem5  35398  erdszelem6  35399  erdszelem7  35400  erdszelem8  35401  filnetlem3  36583  filnetlem4  36584  bj-genr  36885  bj-genl  36886  bj-genan  36887  3lexlogpow5ineq5  42510  aks4d1p1p7  42524  tan3rdpi  42795  cos2t3rdpi  42797  cos4t3rdpi  42799  acos1half  42801  uun0.1  45219  permaxpow  45451  pssnssi  45546  fourierdlem62  46611  fourierdlem68  46617  nthrucw  47329  abcdtb  47371  abcdtc  47372  abcdtd  47373  nabctnabc  47376  zlmodzxzsubm  48832  zlmodzxzldep  48977  ldepsnlinclem1  48978  ldepsnlinclem2  48979  sepfsepc  49400  idfth  49630  idsubc  49632  prstcleval  50027  prstcocval  50029  setc1onsubc  50074