![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > simp2bi | Unicode version |
Description: Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
Ref | Expression |
---|---|
3simp1bi.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
simp2bi |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3simp1bi.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | biimpi 120 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | simp2d 1010 |
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 ax-ia2 107 |
This theorem depends on definitions: df-bi 117 df-3an 980 |
This theorem is referenced by: 0ellim 4397 smodm 6289 erdm 6542 ixpfn 6701 dif1en 6876 eluzelz 9533 elfz3nn0 10110 ef01bndlem 11757 sin01bnd 11758 cos01bnd 11759 sin01gt0 11762 gznegcl 12365 gzcjcl 12366 gzaddcl 12367 gzmulcl 12368 gzabssqcl 12371 4sqlem4a 12381 subgss 12965 srgmgp 13082 ringmgp 13116 reeff1oleme 14064 cosq14gt0 14124 cosq23lt0 14125 coseq0q4123 14126 coseq00topi 14127 coseq0negpitopi 14128 cosq34lt1 14142 cos02pilt1 14143 ioocosf1o 14146 2sqlem2 14322 2sqlem3 14324 |
Copyright terms: Public domain | W3C validator |