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

This theorem is referenced by:  tfr2b  8329  rdgdmlim  8350  oeoa  8527  oeoe  8529  ordtypelem3  9429  ordtypelem5  9431  ordtypelem6  9432  ordtypelem7  9433  ordtypelem9  9435  r1fin  9692  r1tr  9695  r1ordg  9697  r1ord3g  9698  r1pwss  9703  r1val1  9705  rankwflemb  9712  r1elwf  9715  rankr1ai  9717  rankdmr1  9720  rankr1ag  9721  rankr1bg  9722  pwwf  9726  unwf  9729  rankr1clem  9739  rankr1c  9740  rankval3b  9745  rankonidlem  9747  onssr1  9750  rankeq0b  9779  alephsuc2  9997  ackbij2  10159  wunom  10638  negiso  12131  infrenegsup  12134  om2uzoi  13912  faclbnd4lem1  14250  hashunlei  14382  hashsslei  14383  hashle2pr  14434  cos01bnd  16148  cos1bnd  16149  cos2bnd  16150  sincos2sgn  16156  sin4lt0  16157  egt2lt3  16168  divalglem9  16365  bitsinv  16412  drngui  20711  srasca  21174  cnfldfunALT  21366  redvr  21596  refld  21598  iccpnfcnv  24933  xrhmph  24936  recvs  25135  qcvs  25136  i1f1  25679  itg11  25680  dvcos  25972  sinpi  26442  sinhalfpilem  26449  coshalfpi  26455  sincosq1lem  26483  tangtx  26491  sincos4thpi  26499  tan4thpi  26500  tan4thpiOLD  26501  sincos6thpi  26502  sincos3rdpi  26503  pige3ALT  26506  logltb  26586  1cubrlem  26827  1cubr  26828  log2tlbnd  26931  cxploglim2  26964  emcllem6  26986  emcllem7  26987  ppiublem1  27187  ppiublem2  27188  bposlem9  27277  lgsdir2lem4  27313  lgsdir2lem5  27314  chebbnd1lem2  27455  chebbnd1lem3  27456  chebbnd1  27457  dchrvmasumlema  27485  mulog2sumlem2  27520  pntlemb  27582  qdrng  27605  upgrbi  29184  upgr1elem  29203  usgrexmpledg  29353  ntrl2v2e  30250  frgrwopreg2  30411  normlem7tALT  31212  hhsssh  31362  shintcli  31422  chintcli  31424  omlsi  31497  qlaxr3i  31729  lnophm  32112  nmcopex  32122  nmcoplb  32123  nmbdfnlbi  32142  nmcfnex  32146  nmcfnlb  32147  hmopidmch  32246  hmopidmpj  32247  chirred  32488  1fldgenq  33410  zringfrac  33649  esplyind  33771  rrxdim  33810  constrextdg2  33945  constrext2chnlem  33946  2sqr3minply  33976  2sqr3nconstr  33977  cos9thpiminply  33984  cos9thpinconstrlem2  33986  trisecnconstr  33988  xrge0hmph  34128  qqh0  34180  qqh1  34181  rerrext  34205  zrhre  34215  qqhre  34216  mbfmvolf  34462  hgt750lem  34847  r11  35290  r12  35291  subfacval2  35430  erdszelem5  35438  erdszelem6  35439  erdszelem7  35440  erdszelem8  35441  filnetlem3  36623  filnetlem4  36624  bj-genr  36933  bj-genl  36934  bj-genan  36935  3lexlogpow5ineq5  42560  aks4d1p1p7  42574  tan3rdpi  42844  cos2t3rdpi  42846  cos4t3rdpi  42848  acos1half  42850  uun0.1  45236  permaxpow  45468  pssnssi  45562  fourierdlem62  46625  fourierdlem68  46631  nthrucw  47345  abcdtb  47403  abcdtc  47404  abcdtd  47405  nabctnabc  47408  zlmodzxzsubm  48864  zlmodzxzldep  49009  ldepsnlinclem1  49010  ldepsnlinclem2  49011  sepfsepc  49432  idfth  49662  idsubc  49664  prstcleval  50059  prstcocval  50061  setc1onsubc  50106