![]() |
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 4286 ssdomg 6778 negiso 8912 infrenegsupex 9594 xrnegiso 11270 infxrnegsupex 11271 cos01bnd 11766 cos1bnd 11767 cos2bnd 11768 sin4lt0 11774 egt2lt3 11787 epos 11788 ene1 11792 eap1 11793 slotslfn 12488 strslfvd 12504 strslfv2d 12505 strsl0 12511 setsslid 12513 setsslnid 12514 reeff1o 14197 pigt2lt4 14208 pire 14210 pipos 14212 sinhalfpi 14220 tan4thpi 14265 sincos3rdpi 14267 pigt3 14268 lgsdir2lem4 14435 lgsdir2lem5 14436 |
Copyright terms: Public domain | W3C validator |