![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > simp1bi | Unicode version |
Description: Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
Ref | Expression |
---|---|
3simp1bi.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
simp1bi |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3simp1bi.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | biimpi 119 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | simp1d 994 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 |
This theorem depends on definitions: df-bi 116 df-3an 965 |
This theorem is referenced by: limord 4325 smores2 6199 smofvon2dm 6201 smofvon 6204 errel 6446 lincmb01cmp 9816 iccf1o 9817 elfznn0 9925 elfzouz 9959 ef01bndlem 11499 sin01bnd 11500 cos01bnd 11501 sin01gt0 11504 cos01gt0 11505 sin02gt0 11506 coseq00topi 12964 coseq0negpitopi 12965 cosq34lt1 12979 cos11 12982 |
Copyright terms: Public domain | W3C validator |