![]() |
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 4414 smores2 6319 ersym 6571 ertr 6574 fvixp 6729 fiintim 6957 eluzle 9570 ef01bndlem 11796 sin01bnd 11797 cos01bnd 11798 sin01gt0 11801 gznegcl 12407 gzcjcl 12408 gzaddcl 12409 gzmulcl 12410 gzabssqcl 12413 4sqlem4a 12423 ennnfonelemim 12475 xpsff1o 12825 subggrp 13116 srgdilem 13323 srgrz 13338 srglz 13339 ringdilem 13366 ringsrg 13399 subrngss 13547 lmodlema 13608 reeff1oleme 14650 cosq14gt0 14710 cosq23lt0 14711 coseq0q4123 14712 coseq00topi 14713 coseq0negpitopi 14714 cosq34lt1 14728 cos02pilt1 14729 ioocosf1o 14732 2sqlem2 14920 2sqlem3 14922 |
Copyright terms: Public domain | W3C validator |