Theorem simpri 113

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

Syntax hints:   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-ia2 107

This theorem is referenced by:  bi3  119  dfbi2  392  olc  723  mptxor  1473  sb4bor  1888  ordsoexmid  4707  eninl  7431  eninr  7432  pw1ne1  7582  negiso  9279  infrenegsupex  9977  xrnegiso  12011  infxrnegsupex  12012  cos01bnd  12508  cos1bnd  12509  cos2bnd  12510  sincos2sgn  12516  sin4lt0  12517  egt2lt3  12530  ssnnctlemct  13320  slotslfn  13361  strslfvd  13377  strslfv2d  13378  strslfv  13380  strslfv3  13381  strsl0  13384  setsslid  13386  setsslnid  13387  slotm  13398  rngplusgg  13474  rngmulrg  13475  srngplusgd  13485  srngmulrd  13486  srnginvld  13487  lmodplusgd  13503  lmodscad  13504  lmodvscad  13505  ipsaddgd  13515  ipsmulrd  13516  ipsscad  13517  ipsvscad  13518  ipsipd  13519  topgrpplusgd  13535  topgrptsetd  13536  prdsvallem  13604  imasex  13609  imasival  13610  imasbas  13611  imasplusg  13612  imasmulr  13613  prdsex  14155  prdsval  14156  prdssca  14158  prdsmulr  14161  fnmgp  14202  mgpvalg  14203  mgpex  14206  mgpbasg  14207  mgpscag  14209  mgptsetg  14210  mgpdsg  14212  mgpress  14213  ring1  14347  opprvalg  14357  opprex  14361  opprsllem  14362  rmodislmod  14671  sraval  14757  sralemg  14758  srascag  14762  sravscag  14763  sraipg  14764  sraex  14766  zlmval  14945  zlmlemg  14946  zlmmulrg  14949  zlmsca  14950  zlmvscag  14951  znmul  14960  psrval  15033  fnpsr  15034  setsmsdsg  15564  cosz12  15864  sinpi  15869  sinhalfpilem  15875  coshalfpi  15881  sincosq1lem  15909  tangtx  15922  sincos4thpi  15924  tan4thpi  15925  sincos6thpi  15926  sincos3rdpi  15927  pigt3  15928  logltb  15958  log2tlbndlog2  16065  lgsdir2lem4  16133  lgsdir2lem5  16134