![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > simpri | GIF version |
Description: Inference eliminating a conjunct. (Contributed by NM, 15-Jun-1994.) |
Ref | Expression |
---|---|
simpri.1 | ⊢ (𝜑 ∧ 𝜓) |
Ref | Expression |
---|---|
simpri | ⊢ 𝜓 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpri.1 | . 2 ⊢ (𝜑 ∧ 𝜓) | |
2 | simpr 110 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝜓 |
Colors of variables: wff set class |
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 711 mptxor 1424 sb4bor 1835 ordsoexmid 4558 eninl 7090 eninr 7091 pw1ne1 7222 negiso 8898 infrenegsupex 9580 xrnegiso 11251 infxrnegsupex 11252 cos01bnd 11747 cos1bnd 11748 cos2bnd 11749 sincos2sgn 11754 sin4lt0 11755 egt2lt3 11768 ssnnctlemct 12427 slotslfn 12468 strslfvd 12483 strslfv2d 12484 strslfv 12486 strsl0 12490 setsslid 12492 setsslnid 12493 rngplusgg 12571 rngmulrg 12572 srngplusgd 12578 srngmulrd 12579 srnginvld 12580 lmodplusgd 12592 lmodscad 12593 lmodvscad 12594 ipsaddgd 12600 ipsmulrd 12601 ipsscad 12602 ipsvscad 12603 ipsipd 12604 topgrpplusgd 12617 topgrptsetd 12618 fnmgp 12956 mgpvalg 12957 mgpex 12959 mgpbasg 12960 mgpscag 12961 mgptsetg 12962 mgpdsg 12964 ring1 13059 opprvalg 13063 opprex 13067 opprsllem 13068 setsmsdsg 13640 cosz12 13861 sinpi 13866 sinhalfpilem 13872 coshalfpi 13878 sincosq1lem 13906 tangtx 13919 sincos4thpi 13921 tan4thpi 13922 sincos6thpi 13923 sincos3rdpi 13924 pigt3 13925 logltb 13955 lgsdir2lem4 14092 lgsdir2lem5 14093 |
Copyright terms: Public domain | W3C validator |