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 108 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝜑 |
Colors of variables: wff set class |
Syntax hints: ∧ wa 103 |
This theorem was proved from axioms: ax-mp 5 ax-ia1 105 |
This theorem is referenced by: bi1 117 bi2 129 dfbi2 385 orc 686 pwundifss 4177 ssdomg 6640 negiso 8681 infrenegsupex 9357 xrnegiso 10999 infxrnegsupex 11000 cos01bnd 11392 cos1bnd 11393 cos2bnd 11394 sin4lt0 11400 egt2lt3 11413 epos 11414 ene1 11418 eap1 11419 slotslfn 11912 strslfvd 11927 strslfv2d 11928 strsl0 11934 setsslid 11936 setsslnid 11937 pigt2lt4 12792 pire 12794 pipos 12796 sinhalfpi 12804 tan4thpi 12849 sincos3rdpi 12851 pigt3 12852 |
Copyright terms: Public domain | W3C validator |