![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > simpli | GIF version |
Description: Inference eliminating a conjunct. (Contributed by NM, 15-Jun-1994.) |
Ref | Expression |
---|---|
simpli.1 | ⊢ (𝜑 ∧ 𝜓) |
Ref | Expression |
---|---|
simpli | ⊢ 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpli.1 | . 2 ⊢ (𝜑 ∧ 𝜓) | |
2 | simpl 109 | . 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-ia1 106 |
This theorem is referenced by: biimp 118 biimpr 130 dfbi2 388 orc 712 pwundifss 4287 ssdomg 6780 negiso 8914 infrenegsupex 9596 xrnegiso 11272 infxrnegsupex 11273 cos01bnd 11768 cos1bnd 11769 cos2bnd 11770 sin4lt0 11776 egt2lt3 11789 epos 11790 ene1 11794 eap1 11795 slotslfn 12490 strslfvd 12506 strslfv2d 12507 strsl0 12513 setsslid 12515 setsslnid 12516 reeff1o 14233 pigt2lt4 14244 pire 14246 pipos 14248 sinhalfpi 14256 tan4thpi 14301 sincos3rdpi 14303 pigt3 14304 lgsdir2lem4 14471 lgsdir2lem5 14472 |
Copyright terms: Public domain | W3C validator |