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 1004 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 w3a 973 |
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 975 |
This theorem is referenced by: limord 4378 smores2 6270 smofvon2dm 6272 smofvon 6275 errel 6518 lincmb01cmp 9947 iccf1o 9948 elfznn0 10057 elfzouz 10094 ef01bndlem 11706 sin01bnd 11707 cos01bnd 11708 sin01gt0 11711 cos01gt0 11712 sin02gt0 11713 eulerthlema 12171 modprm0 12195 gzcn 12311 coseq00topi 13509 coseq0negpitopi 13510 cosq34lt1 13524 cos11 13527 nconstwlpolemgt0 14055 |
Copyright terms: Public domain | W3C validator |