Theorem simpri 486

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 485	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
3	1, 2	ax-mp 5	1 ⊢ 𝜓

Syntax hints:   ∧ wa 396

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 397

This theorem is referenced by:  tfr2b  8236  rdgdmlim  8257  oeoa  8437  oeoe  8439  ordtypelem3  9288  ordtypelem5  9290  ordtypelem6  9291  ordtypelem7  9292  ordtypelem9  9294  r1fin  9540  r1tr  9543  r1ordg  9545  r1ord3g  9546  r1pwss  9551  r1val1  9553  rankwflemb  9560  r1elwf  9563  rankr1ai  9565  rankdmr1  9568  rankr1ag  9569  rankr1bg  9570  pwwf  9574  unwf  9577  rankr1clem  9587  rankr1c  9588  rankval3b  9593  rankonidlem  9595  onssr1  9598  rankeq0b  9627  alephsuc2  9845  ackbij2  10008  wunom  10485  negiso  11964  infrenegsup  11967  om2uzoi  13684  faclbnd4lem1  14016  hashunlei  14149  hashsslei  14150  hashle2pr  14200  cos01bnd  15904  cos1bnd  15905  cos2bnd  15906  sincos2sgn  15912  sin4lt0  15913  egt2lt3  15924  divalglem9  16119  bitsinv  16164  drngui  20006  srasca  20456  cnfldfunALT  20619  redvr  20831  refld  20833  recrng  20835  iccpnfcnv  24116  xrhmph  24119  recvs  24318  recvsOLD  24319  qcvs  24320  i1f1  24863  itg11  24864  dvcos  25156  sinpi  25623  sinhalfpilem  25629  coshalfpi  25635  sincosq1lem  25663  tangtx  25671  sincos4thpi  25679  tan4thpi  25680  sincos6thpi  25681  sincos3rdpi  25682  pige3ALT  25685  logltb  25764  1cubrlem  26000  1cubr  26001  log2tlbnd  26104  cxploglim2  26137  emcllem6  26159  emcllem7  26160  ppiublem1  26359  ppiublem2  26360  bposlem9  26449  lgsdir2lem4  26485  lgsdir2lem5  26486  chebbnd1lem2  26627  chebbnd1lem3  26628  chebbnd1  26629  dchrvmasumlema  26657  mulog2sumlem2  26692  pntlemb  26754  qdrng  26777  upgrbi  27472  upgr1elem  27491  usgrexmpledg  27638  ntrl2v2e  28531  frgrwopreg2  28692  normlem7tALT  29490  hhsssh  29640  shintcli  29700  chintcli  29702  omlsi  29775  qlaxr3i  30007  lnophm  30390  nmcopex  30400  nmcoplb  30401  nmbdfnlbi  30420  nmcfnex  30424  nmcfnlb  30425  hmopidmch  30524  hmopidmpj  30525  chirred  30766  rrxdim  31706  xrge0hmph  31891  qqh0  31943  qqh1  31944  rerrext  31968  zrhre  31978  qqhre  31979  mbfmvolf  32242  hgt750lem  32640  subfacval2  33158  erdszelem5  33166  erdszelem6  33167  erdszelem7  33168  erdszelem8  33169  filnetlem3  34578  filnetlem4  34579  bj-genr  34797  bj-genl  34798  bj-genan  34799  3lexlogpow5ineq5  40075  aks4d1p1p7  40089  acos1half  40177  uun0.1  42405  pssnssi  42658  fourierdlem62  43716  fourierdlem68  43722  abcdtb  44432  abcdtc  44433  abcdtd  44434  nabctnabc  44437  zlmodzxzsubm  45706  zlmodzxzldep  45856  ldepsnlinclem1  45857  ldepsnlinclem2  45858  sepfsepc  46232  prstcleval  46360  prstcocval  46363