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 707 pwundifss 4270 ssdomg 6756 negiso 8871 infrenegsupex 9553 xrnegiso 11225 infxrnegsupex 11226 cos01bnd 11721 cos1bnd 11722 cos2bnd 11723 sin4lt0 11729 egt2lt3 11742 epos 11743 ene1 11747 eap1 11748 slotslfn 12442 strslfvd 12457 strslfv2d 12458 strsl0 12464 setsslid 12466 setsslnid 12467 reeff1o 13488 pigt2lt4 13499 pire 13501 pipos 13503 sinhalfpi 13511 tan4thpi 13556 sincos3rdpi 13558 pigt3 13559 lgsdir2lem4 13726 lgsdir2lem5 13727 |
Copyright terms: Public domain | W3C validator |