![]() |
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 1012 |
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 982 |
This theorem is referenced by: 0ellim 4429 smodm 6344 erdm 6597 ixpfn 6758 dif1en 6935 eluzelz 9601 elfz3nn0 10181 ef01bndlem 11899 sin01bnd 11900 cos01bnd 11901 sin01gt0 11905 gznegcl 12513 gzcjcl 12514 gzaddcl 12515 gzmulcl 12516 gzabssqcl 12519 4sqlem4a 12529 xpsff1o 12932 subgss 13244 rngmgp 13432 srgmgp 13464 ringmgp 13498 lmodring 13791 lmodprop2d 13844 reeff1oleme 14907 cosq14gt0 14967 cosq23lt0 14968 coseq0q4123 14969 coseq00topi 14970 coseq0negpitopi 14971 cosq34lt1 14985 cos02pilt1 14986 ioocosf1o 14989 gausslemma2dlem1a 15174 2sqlem2 15202 2sqlem3 15204 |
Copyright terms: Public domain | W3C validator |