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

This theorem is referenced by:  tfr2b  8198  rdgdmlim  8219  oeoa  8390  oeoe  8392  ordtypelem3  9209  ordtypelem5  9211  ordtypelem6  9212  ordtypelem7  9213  ordtypelem9  9215  r1fin  9462  r1tr  9465  r1ordg  9467  r1ord3g  9468  r1pwss  9473  r1val1  9475  rankwflemb  9482  r1elwf  9485  rankr1ai  9487  rankdmr1  9490  rankr1ag  9491  rankr1bg  9492  pwwf  9496  unwf  9499  rankr1clem  9509  rankr1c  9510  rankval3b  9515  rankonidlem  9517  onssr1  9520  rankeq0b  9549  alephsuc2  9767  ackbij2  9930  wunom  10407  negiso  11885  infrenegsup  11888  om2uzoi  13603  faclbnd4lem1  13935  hashunlei  14068  hashsslei  14069  hashle2pr  14119  cos01bnd  15823  cos1bnd  15824  cos2bnd  15825  sincos2sgn  15831  sin4lt0  15832  egt2lt3  15843  divalglem9  16038  bitsinv  16083  drngui  19912  redvr  20734  refld  20736  recrng  20738  iccpnfcnv  24013  xrhmph  24016  recvs  24215  qcvs  24216  i1f1  24759  itg11  24760  dvcos  25052  sinpi  25519  sinhalfpilem  25525  coshalfpi  25531  sincosq1lem  25559  tangtx  25567  sincos4thpi  25575  tan4thpi  25576  sincos6thpi  25577  sincos3rdpi  25578  pige3ALT  25581  logltb  25660  1cubrlem  25896  1cubr  25897  log2tlbnd  26000  cxploglim2  26033  emcllem6  26055  emcllem7  26056  ppiublem1  26255  ppiublem2  26256  bposlem9  26345  lgsdir2lem4  26381  lgsdir2lem5  26382  chebbnd1lem2  26523  chebbnd1lem3  26524  chebbnd1  26525  dchrvmasumlema  26553  mulog2sumlem2  26588  pntlemb  26650  qdrng  26673  upgrbi  27366  upgr1elem  27385  usgrexmpledg  27532  ntrl2v2e  28423  frgrwopreg2  28584  normlem7tALT  29382  hhsssh  29532  shintcli  29592  chintcli  29594  omlsi  29667  qlaxr3i  29899  lnophm  30282  nmcopex  30292  nmcoplb  30293  nmbdfnlbi  30312  nmcfnex  30316  nmcfnlb  30317  hmopidmch  30416  hmopidmpj  30417  chirred  30658  rrxdim  31599  xrge0hmph  31784  qqh0  31834  qqh1  31835  rerrext  31859  zrhre  31869  qqhre  31870  mbfmvolf  32133  hgt750lem  32531  subfacval2  33049  erdszelem5  33057  erdszelem6  33058  erdszelem7  33059  erdszelem8  33060  filnetlem3  34496  filnetlem4  34497  bj-genr  34715  bj-genl  34716  bj-genan  34717  3lexlogpow5ineq5  39996  aks4d1p1p7  40010  acos1half  40098  uun0.1  42287  pssnssi  42540  fourierdlem62  43599  fourierdlem68  43605  abcdtb  44308  abcdtc  44309  abcdtd  44310  nabctnabc  44313  zlmodzxzsubm  45583  zlmodzxzldep  45733  ldepsnlinclem1  45734  ldepsnlinclem2  45735  sepfsepc  46109