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: biimp 117 biimpr 129 dfbi2 386 orc 702 pwundifss 4247 ssdomg 6725 negiso 8831 infrenegsupex 9510 xrnegiso 11170 infxrnegsupex 11171 cos01bnd 11666 cos1bnd 11667 cos2bnd 11668 sin4lt0 11674 egt2lt3 11687 epos 11688 ene1 11692 eap1 11693 slotslfn 12286 strslfvd 12301 strslfv2d 12302 strsl0 12308 setsslid 12310 setsslnid 12311 reeff1o 13164 pigt2lt4 13175 pire 13177 pipos 13179 sinhalfpi 13187 tan4thpi 13232 sincos3rdpi 13234 pigt3 13235 |
Copyright terms: Public domain | W3C validator |