| 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 120 |
. 2
|
| 3 | 2 | simp3d 1013 |
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 ax-ia3 108 |
| This theorem depends on definitions: df-bi 117 df-3an 982 |
| This theorem is referenced by: limuni 4442 smores2 6379 ersym 6631 ertr 6634 fvixp 6789 en2 6911 fiintim 7027 eluzle 9659 ef01bndlem 12038 sin01bnd 12039 cos01bnd 12040 sin01gt0 12044 gznegcl 12669 gzcjcl 12670 gzaddcl 12671 gzmulcl 12672 gzabssqcl 12675 4sqlem4a 12685 ennnfonelemim 12766 prdsbasprj 13085 xpsff1o 13152 subggrp 13484 srgdilem 13702 srgrz 13717 srglz 13718 ringdilem 13745 ringsrg 13780 subrngss 13933 lmodlema 14025 reeff1oleme 15215 cosq14gt0 15275 cosq23lt0 15276 coseq0q4123 15277 coseq00topi 15278 coseq0negpitopi 15279 cosq34lt1 15293 cos02pilt1 15294 ioocosf1o 15297 2sqlem2 15563 2sqlem3 15565 |
| Copyright terms: Public domain | W3C validator |