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  8310  rdgdmlim  8331  oeoa  8507  oeoe  8509  ordtypelem3  9401  ordtypelem5  9403  ordtypelem6  9404  ordtypelem7  9405  ordtypelem9  9407  r1fin  9658  r1tr  9661  r1ordg  9663  r1ord3g  9664  r1pwss  9669  r1val1  9671  rankwflemb  9678  r1elwf  9681  rankr1ai  9683  rankdmr1  9686  rankr1ag  9687  rankr1bg  9688  pwwf  9692  unwf  9695  rankr1clem  9705  rankr1c  9706  rankval3b  9711  rankonidlem  9713  onssr1  9716  rankeq0b  9745  alephsuc2  9963  ackbij2  10125  wunom  10603  negiso  12094  infrenegsup  12097  om2uzoi  13854  faclbnd4lem1  14192  hashunlei  14324  hashsslei  14325  hashle2pr  14376  cos01bnd  16087  cos1bnd  16088  cos2bnd  16089  sincos2sgn  16095  sin4lt0  16096  egt2lt3  16107  divalglem9  16304  bitsinv  16351  drngui  20643  srasca  21107  cnfldfunALT  21299  cnfldfunALTOLD  21312  redvr  21547  refld  21549  iccpnfcnv  24862  xrhmph  24865  recvs  25066  qcvs  25067  i1f1  25611  itg11  25612  dvcos  25907  sinpi  26385  sinhalfpilem  26392  coshalfpi  26398  sincosq1lem  26426  tangtx  26434  sincos4thpi  26442  tan4thpi  26443  tan4thpiOLD  26444  sincos6thpi  26445  sincos3rdpi  26446  pige3ALT  26449  logltb  26529  1cubrlem  26771  1cubr  26772  log2tlbnd  26875  cxploglim2  26909  emcllem6  26931  emcllem7  26932  ppiublem1  27133  ppiublem2  27134  bposlem9  27223  lgsdir2lem4  27259  lgsdir2lem5  27260  chebbnd1lem2  27401  chebbnd1lem3  27402  chebbnd1  27403  dchrvmasumlema  27431  mulog2sumlem2  27466  pntlemb  27528  qdrng  27551  upgrbi  29064  upgr1elem  29083  usgrexmpledg  29233  ntrl2v2e  30128  frgrwopreg2  30289  normlem7tALT  31089  hhsssh  31239  shintcli  31299  chintcli  31301  omlsi  31374  qlaxr3i  31606  lnophm  31989  nmcopex  31999  nmcoplb  32000  nmbdfnlbi  32019  nmcfnex  32023  nmcfnlb  32024  hmopidmch  32123  hmopidmpj  32124  chirred  32365  1fldgenq  33278  zringfrac  33509  rrxdim  33617  constrextdg2  33752  constrext2chnlem  33753  2sqr3minply  33783  2sqr3nconstr  33784  cos9thpiminply  33791  cos9thpinconstrlem2  33793  trisecnconstr  33795  xrge0hmph  33935  qqh0  33987  qqh1  33988  rerrext  34012  zrhre  34022  qqhre  34023  mbfmvolf  34269  hgt750lem  34654  subfacval2  35199  erdszelem5  35207  erdszelem6  35208  erdszelem7  35209  erdszelem8  35210  filnetlem3  36393  filnetlem4  36394  bj-genr  36619  bj-genl  36620  bj-genan  36621  3lexlogpow5ineq5  42072  aks4d1p1p7  42086  tan3rdpi  42364  cos2t3rdpi  42366  cos4t3rdpi  42368  acos1half  42370  uun0.1  44789  permaxpow  45021  pssnssi  45117  fourierdlem62  46185  fourierdlem68  46191  abcdtb  46936  abcdtc  46937  abcdtd  46938  nabctnabc  46941  zlmodzxzsubm  48369  zlmodzxzldep  48515  ldepsnlinclem1  48516  ldepsnlinclem2  48517  sepfsepc  48938  idfth  49169  idsubc  49171  prstcleval  49566  prstcocval  49568  setc1onsubc  49613