Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > simp3bi | Unicode version |
Description: Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
Ref | Expression |
---|---|
3simp1bi.1 |
Ref | Expression |
---|---|
simp3bi |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3simp1bi.1 | . . 3 | |
2 | 1 | biimpi 119 | . 2 |
3 | 2 | simp3d 980 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 w3a 947 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 949 |
This theorem is referenced by: limuni 4288 smores2 6159 ersym 6409 ertr 6412 fvixp 6565 fiintim 6785 eluzle 9306 ef01bndlem 11390 sin01bnd 11391 cos01bnd 11392 sin01gt0 11395 ennnfonelemim 11864 cosq14gt0 12840 cosq23lt0 12841 coseq0q4123 12842 coseq00topi 12843 coseq0negpitopi 12844 cosq34lt1 12858 cos02pilt1 12859 |
Copyright terms: Public domain | W3C validator |