![]() |
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 120 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | simp1d 1011 |
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 106 |
This theorem depends on definitions: df-bi 117 df-3an 982 |
This theorem is referenced by: limord 4413 smores2 6319 smofvon2dm 6321 smofvon 6324 errel 6568 lincmb01cmp 10033 iccf1o 10034 elfznn0 10144 elfzouz 10181 ef01bndlem 11796 sin01bnd 11797 cos01bnd 11798 sin01gt0 11801 cos01gt0 11802 sin02gt0 11803 eulerthlema 12262 modprm0 12286 gzcn 12404 subgbas 13117 subgrcl 13118 rngabl 13289 srgcmn 13320 ringgrp 13355 subrngrcl 13550 lmodgrp 13610 coseq00topi 14713 coseq0negpitopi 14714 cosq34lt1 14728 cos11 14731 nconstwlpolemgt0 15271 |
Copyright terms: Public domain | W3C validator |