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  388  olc  712  mptxor  1435  sb4bor  1849  ordsoexmid  4599  eninl  7172  eninr  7173  pw1ne1  7314  negiso  9001  infrenegsupex  9687  xrnegiso  11446  infxrnegsupex  11447  cos01bnd  11942  cos1bnd  11943  cos2bnd  11944  sincos2sgn  11950  sin4lt0  11951  egt2lt3  11964  ssnnctlemct  12690  slotslfn  12731  strslfvd  12747  strslfv2d  12748  strslfv  12750  strslfv3  12751  strsl0  12754  setsslid  12756  setsslnid  12757  rngplusgg  12841  rngmulrg  12842  srngplusgd  12852  srngmulrd  12853  srnginvld  12854  lmodplusgd  12870  lmodscad  12871  lmodvscad  12872  ipsaddgd  12882  ipsmulrd  12883  ipsscad  12884  ipsvscad  12885  ipsipd  12886  topgrpplusgd  12902  topgrptsetd  12903  prdsex  12973  prdsvallem  12976  prdsval  12977  prdssca  12979  prdsmulr  12982  imasex  13009  imasival  13010  imasbas  13011  imasplusg  13012  imasmulr  13013  fnmgp  13556  mgpvalg  13557  mgpex  13559  mgpbasg  13560  mgpscag  13561  mgptsetg  13562  mgpdsg  13564  mgpress  13565  ring1  13693  opprvalg  13703  opprex  13707  opprsllem  13708  rmodislmod  13985  sraval  14071  sralemg  14072  srascag  14076  sravscag  14077  sraipg  14078  sraex  14080  zlmval  14261  zlmlemg  14262  zlmmulrg  14265  zlmsca  14266  zlmvscag  14267  znmul  14276  psrval  14298  fnpsr  14299  setsmsdsg  14802  cosz12  15102  sinpi  15107  sinhalfpilem  15113  coshalfpi  15119  sincosq1lem  15147  tangtx  15160  sincos4thpi  15162  tan4thpi  15163  sincos6thpi  15164  sincos3rdpi  15165  pigt3  15166  logltb  15196  lgsdir2lem4  15358  lgsdir2lem5  15359