Theorem simpri 491

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

This proof depends on syntax axioms:   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  tfr2b  8388  rdgdmlim  8409  oeoa  8588  oeoe  8590  ordtypelem3  9495  ordtypelem5  9497  ordtypelem6  9498  ordtypelem7  9499  ordtypelem9  9501  r1fin  9758  r1tr  9761  r1ordg  9763  r1ord3g  9764  r1pwss  9769  r1val1  9771  rankwflemb  9778  r1elwf  9781  rankr1ai  9783  rankdmr1  9786  rankr1ag  9787  rankr1bg  9788  pwwf  9792  unwf  9795  rankr1clem  9805  rankr1c  9806  rankval3b  9811  rankonidlem  9813  onssr1  9816  rankeq0b  9845  alephsuc2  10086  ackbij2  10247  wunom  10732  negiso  12222  infrenegsup  12225  om2uzoi  14021  faclbnd4lem1  14359  hashunlei  14492  hashsslei  14493  hashle2pr  14544  cos01bnd  16278  cos1bnd  16279  cos2bnd  16280  sincos2sgn  16286  sin4lt0  16287  egt2lt3  16298  divalglem9  16495  bitsinv  16542  drngui  20900  srasca  21368  cnfldfunALT  21604  redvr  21834  refld  21836  iccpnfcnv  25176  xrhmph  25179  recvs  25378  qcvs  25379  i1f1  25922  itg11  25923  dvcos  26215  sinpi  26691  sinhalfpilem  26701  coshalfpi  26707  sincosq1lem  26735  tangtx  26743  sincos4thpi  26751  tan4thpi  26752  tan4thpiOLD  26753  sincos6thpi  26754  sincos3rdpi  26755  pige3ALT  26758  logltb  26838  1cubrlem  27079  1cubr  27080  log2tlbnd  27183  cxploglim2  27216  emcllem6  27238  emcllem7  27239  ppiublem1  27439  ppiublem2  27440  bposlem9  27529  lgsdir2lem4  27565  lgsdir2lem5  27566  chebbnd1lem2  27707  chebbnd1lem3  27708  chebbnd1  27709  dchrvmasumlema  27737  mulog2sumlem2  27772  pntlemb  27834  qdrng  27857  upgrbi  29551  upgr1elem  29570  usgrexmpledg  29723  ntrl2v2e  30639  frgrwopreg2  30800  normlem7tALT  31601  hhsssh  31751  shintcli  31811  chintcli  31813  omlsi  31886  qlaxr3i  32118  lnophm  32501  nmcopex  32511  nmcoplb  32512  nmbdfnlbi  32531  nmcfnex  32535  nmcfnlb  32536  hmopidmch  32635  hmopidmpj  32636  chirred  32877  1fldgenq  33765  zringfrac  33966  esplyind  34087  rrxdim  34126  constrextdg2  34261  constrext2chnlem  34262  2sqr3minply  34292  2sqr3nconstr  34293  cos9thpiminply  34300  cos9thpinconstrlem2  34302  trisecnconstr  34304  xrge0hmph  34444  qqh0  34496  qqh1  34497  rerrext  34521  zrhre  34531  qqhre  34532  mbfmvolf  34779  hgt750lem  35161  r11  35603  r12  35604  subfacval2  35768  erdszelem5  35776  erdszelem6  35777  erdszelem7  35778  erdszelem8  35779  filnetlem3  37001  filnetlem4  37002  bj-genr  37310  bj-genl  37311  bj-genan  37312  3lexlogpow5ineq5  42928  aks4d1p1p7  42942  tan3rdpi  43229  cos2t3rdpi  43231  cos4t3rdpi  43233  acos1half  43235  uun0.1  45602  permaxpow  45834  pssnssi  45935  fourierdlem62  46998  fourierdlem68  47004  numtowerdt  47736  abcdtb  47816  abcdtc  47817  abcdtd  47818  nabctnabc  47821  zlmodzxzsubm  49291  zlmodzxzldep  49436  ldepsnlinclem1  49437  ldepsnlinclem2  49438  sepfsepc  49856  idfth  50086  idsubc  50088  prstcleval  50483  prstcocval  50485  setc1onsubc  50530  veroquaddetzerod  50821