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  8329  rdgdmlim  8350  oeoa  8527  oeoe  8529  ordtypelem3  9429  ordtypelem5  9431  ordtypelem6  9432  ordtypelem7  9433  ordtypelem9  9435  r1fin  9689  r1tr  9692  r1ordg  9694  r1ord3g  9695  r1pwss  9700  r1val1  9702  rankwflemb  9709  r1elwf  9712  rankr1ai  9714  rankdmr1  9717  rankr1ag  9718  rankr1bg  9719  pwwf  9723  unwf  9726  rankr1clem  9736  rankr1c  9737  rankval3b  9742  rankonidlem  9744  onssr1  9747  rankeq0b  9776  alephsuc2  9994  ackbij2  10156  wunom  10635  negiso  12126  infrenegsup  12129  om2uzoi  13882  faclbnd4lem1  14220  hashunlei  14352  hashsslei  14353  hashle2pr  14404  cos01bnd  16115  cos1bnd  16116  cos2bnd  16117  sincos2sgn  16123  sin4lt0  16124  egt2lt3  16135  divalglem9  16332  bitsinv  16379  drngui  20672  srasca  21136  cnfldfunALT  21328  cnfldfunALTOLD  21341  redvr  21576  refld  21578  iccpnfcnv  24902  xrhmph  24905  recvs  25106  qcvs  25107  i1f1  25651  itg11  25652  dvcos  25947  sinpi  26425  sinhalfpilem  26432  coshalfpi  26438  sincosq1lem  26466  tangtx  26474  sincos4thpi  26482  tan4thpi  26483  tan4thpiOLD  26484  sincos6thpi  26485  sincos3rdpi  26486  pige3ALT  26489  logltb  26569  1cubrlem  26811  1cubr  26812  log2tlbnd  26915  cxploglim2  26949  emcllem6  26971  emcllem7  26972  ppiublem1  27173  ppiublem2  27174  bposlem9  27263  lgsdir2lem4  27299  lgsdir2lem5  27300  chebbnd1lem2  27441  chebbnd1lem3  27442  chebbnd1  27443  dchrvmasumlema  27471  mulog2sumlem2  27506  pntlemb  27568  qdrng  27591  upgrbi  29149  upgr1elem  29168  usgrexmpledg  29318  ntrl2v2e  30216  frgrwopreg2  30377  normlem7tALT  31177  hhsssh  31327  shintcli  31387  chintcli  31389  omlsi  31462  qlaxr3i  31694  lnophm  32077  nmcopex  32087  nmcoplb  32088  nmbdfnlbi  32107  nmcfnex  32111  nmcfnlb  32112  hmopidmch  32211  hmopidmpj  32212  chirred  32453  1fldgenq  33385  zringfrac  33616  esplyind  33712  rrxdim  33752  constrextdg2  33887  constrext2chnlem  33888  2sqr3minply  33918  2sqr3nconstr  33919  cos9thpiminply  33926  cos9thpinconstrlem2  33928  trisecnconstr  33930  xrge0hmph  34070  qqh0  34122  qqh1  34123  rerrext  34147  zrhre  34157  qqhre  34158  mbfmvolf  34404  hgt750lem  34789  r11  35231  r12  35232  subfacval2  35362  erdszelem5  35370  erdszelem6  35371  erdszelem7  35372  erdszelem8  35373  filnetlem3  36555  filnetlem4  36556  bj-genr  36781  bj-genl  36782  bj-genan  36783  3lexlogpow5ineq5  42351  aks4d1p1p7  42365  tan3rdpi  42643  cos2t3rdpi  42645  cos4t3rdpi  42647  acos1half  42649  uun0.1  45054  permaxpow  45286  pssnssi  45381  fourierdlem62  46448  fourierdlem68  46454  nthrucw  47166  abcdtb  47208  abcdtc  47209  abcdtd  47210  nabctnabc  47213  zlmodzxzsubm  48641  zlmodzxzldep  48786  ldepsnlinclem1  48787  ldepsnlinclem2  48788  sepfsepc  49209  idfth  49439  idsubc  49441  prstcleval  49836  prstcocval  49838  setc1onsubc  49883