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  8452  rdgdmlim  8473  oeoa  8653  oeoe  8655  ordtypelem3  9589  ordtypelem5  9591  ordtypelem6  9592  ordtypelem7  9593  ordtypelem9  9595  r1fin  9842  r1tr  9845  r1ordg  9847  r1ord3g  9848  r1pwss  9853  r1val1  9855  rankwflemb  9862  r1elwf  9865  rankr1ai  9867  rankdmr1  9870  rankr1ag  9871  rankr1bg  9872  pwwf  9876  unwf  9879  rankr1clem  9889  rankr1c  9890  rankval3b  9895  rankonidlem  9897  onssr1  9900  rankeq0b  9929  alephsuc2  10149  ackbij2  10311  wunom  10789  negiso  12275  infrenegsup  12278  om2uzoi  14006  faclbnd4lem1  14342  hashunlei  14474  hashsslei  14475  hashle2pr  14526  cos01bnd  16234  cos1bnd  16235  cos2bnd  16236  sincos2sgn  16242  sin4lt0  16243  egt2lt3  16254  divalglem9  16449  bitsinv  16494  drngui  20757  srasca  21206  cnfldfunALT  21402  cnfldfunALTOLD  21415  redvr  21658  refld  21660  iccpnfcnv  24994  xrhmph  24997  recvs  25198  recvsOLD  25199  qcvs  25200  i1f1  25744  itg11  25745  dvcos  26041  sinpi  26517  sinhalfpilem  26523  coshalfpi  26529  sincosq1lem  26557  tangtx  26565  sincos4thpi  26573  tan4thpi  26574  tan4thpiOLD  26575  sincos6thpi  26576  sincos3rdpi  26577  pige3ALT  26580  logltb  26660  1cubrlem  26902  1cubr  26903  log2tlbnd  27006  cxploglim2  27040  emcllem6  27062  emcllem7  27063  ppiublem1  27264  ppiublem2  27265  bposlem9  27354  lgsdir2lem4  27390  lgsdir2lem5  27391  chebbnd1lem2  27532  chebbnd1lem3  27533  chebbnd1  27534  dchrvmasumlema  27562  mulog2sumlem2  27597  pntlemb  27659  qdrng  27682  upgrbi  29128  upgr1elem  29147  usgrexmpledg  29297  ntrl2v2e  30190  frgrwopreg2  30351  normlem7tALT  31151  hhsssh  31301  shintcli  31361  chintcli  31363  omlsi  31436  qlaxr3i  31668  lnophm  32051  nmcopex  32061  nmcoplb  32062  nmbdfnlbi  32081  nmcfnex  32085  nmcfnlb  32086  hmopidmch  32185  hmopidmpj  32186  chirred  32427  1fldgenq  33289  zringfrac  33547  rrxdim  33627  2sqr3minply  33738  xrge0hmph  33878  qqh0  33930  qqh1  33931  rerrext  33955  zrhre  33965  qqhre  33966  mbfmvolf  34231  hgt750lem  34628  subfacval2  35155  erdszelem5  35163  erdszelem6  35164  erdszelem7  35165  erdszelem8  35166  filnetlem3  36346  filnetlem4  36347  bj-genr  36572  bj-genl  36573  bj-genan  36574  3lexlogpow5ineq5  42017  aks4d1p1p7  42031  tan3rdpi  42338  acos1half  42340  uun0.1  44749  pssnssi  45003  fourierdlem62  46089  fourierdlem68  46095  abcdtb  46841  abcdtc  46842  abcdtd  46843  nabctnabc  46846  zlmodzxzsubm  48084  zlmodzxzldep  48233  ldepsnlinclem1  48234  ldepsnlinclem2  48235  sepfsepc  48607  prstcleval  48735  prstcocval  48738