![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3impia | Unicode version |
Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.) |
Ref | Expression |
---|---|
3impia.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3impia |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3impia.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | ex 108 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | 3imp 1097 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 df-3an 886 |
This theorem is referenced by: mopick2 1980 3gencl 2582 mob2 2715 moi 2718 reupick3 3216 disjne 3267 funopg 4877 fvun1 5182 fvopab6 5207 isores3 5398 ovmpt4g 5565 ovmpt2s 5566 ov2gf 5567 ofrval 5664 poxp 5794 smoel 5856 nnaass 6003 qsel 6119 xpdom3m 6244 prarloclem3 6480 aptisr 6705 axpre-apti 6769 axapti 6887 divvalap 7435 letrp1 7595 p1le 7596 zextle 8107 zextlt 8108 btwnnz 8110 gtndiv 8111 uzind2 8126 fzind 8129 iccleub 8570 uzsubsubfz 8681 elfz0fzfz0 8753 difelfznle 8763 elfzo0le 8811 fzonmapblen 8813 fzofzim 8814 fzosplitprm1 8860 expcl2lemap 8921 expclzaplem 8933 expnegzap 8943 leexp2r 8962 expnbnd 9025 |
Copyright terms: Public domain | W3C validator |