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  8434  rdgdmlim  8455  oeoa  8633  oeoe  8635  ordtypelem3  9557  ordtypelem5  9559  ordtypelem6  9560  ordtypelem7  9561  ordtypelem9  9563  r1fin  9810  r1tr  9813  r1ordg  9815  r1ord3g  9816  r1pwss  9821  r1val1  9823  rankwflemb  9830  r1elwf  9833  rankr1ai  9835  rankdmr1  9838  rankr1ag  9839  rankr1bg  9840  pwwf  9844  unwf  9847  rankr1clem  9857  rankr1c  9858  rankval3b  9863  rankonidlem  9865  onssr1  9868  rankeq0b  9897  alephsuc2  10117  ackbij2  10279  wunom  10757  negiso  12245  infrenegsup  12248  om2uzoi  13992  faclbnd4lem1  14328  hashunlei  14460  hashsslei  14461  hashle2pr  14512  cos01bnd  16218  cos1bnd  16219  cos2bnd  16220  sincos2sgn  16226  sin4lt0  16227  egt2lt3  16238  divalglem9  16434  bitsinv  16481  drngui  20751  srasca  21200  cnfldfunALT  21396  cnfldfunALTOLD  21409  redvr  21652  refld  21654  iccpnfcnv  24988  xrhmph  24991  recvs  25192  recvsOLD  25193  qcvs  25194  i1f1  25738  itg11  25739  dvcos  26035  sinpi  26513  sinhalfpilem  26519  coshalfpi  26525  sincosq1lem  26553  tangtx  26561  sincos4thpi  26569  tan4thpi  26570  tan4thpiOLD  26571  sincos6thpi  26572  sincos3rdpi  26573  pige3ALT  26576  logltb  26656  1cubrlem  26898  1cubr  26899  log2tlbnd  27002  cxploglim2  27036  emcllem6  27058  emcllem7  27059  ppiublem1  27260  ppiublem2  27261  bposlem9  27350  lgsdir2lem4  27386  lgsdir2lem5  27387  chebbnd1lem2  27528  chebbnd1lem3  27529  chebbnd1  27530  dchrvmasumlema  27558  mulog2sumlem2  27593  pntlemb  27655  qdrng  27678  upgrbi  29124  upgr1elem  29143  usgrexmpledg  29293  ntrl2v2e  30186  frgrwopreg2  30347  normlem7tALT  31147  hhsssh  31297  shintcli  31357  chintcli  31359  omlsi  31432  qlaxr3i  31664  lnophm  32047  nmcopex  32057  nmcoplb  32058  nmbdfnlbi  32077  nmcfnex  32081  nmcfnlb  32082  hmopidmch  32181  hmopidmpj  32182  chirred  32423  1fldgenq  33303  zringfrac  33561  rrxdim  33641  2sqr3minply  33752  xrge0hmph  33892  qqh0  33946  qqh1  33947  rerrext  33971  zrhre  33981  qqhre  33982  mbfmvolf  34247  hgt750lem  34644  subfacval2  35171  erdszelem5  35179  erdszelem6  35180  erdszelem7  35181  erdszelem8  35182  filnetlem3  36362  filnetlem4  36363  bj-genr  36588  bj-genl  36589  bj-genan  36590  3lexlogpow5ineq5  42041  aks4d1p1p7  42055  tan3rdpi  42364  acos1half  42366  uun0.1  44775  pssnssi  45040  fourierdlem62  46123  fourierdlem68  46129  abcdtb  46875  abcdtc  46876  abcdtd  46877  nabctnabc  46880  zlmodzxzsubm  48203  zlmodzxzldep  48349  ldepsnlinclem1  48350  ldepsnlinclem2  48351  sepfsepc  48723  prstcleval  48868  prstcocval  48871