![]() |
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 115 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | 3imp 1193 |
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 980 |
This theorem is referenced by: mopick2 2109 3gencl 2771 mob2 2917 moi 2920 reupick3 3420 disjne 3476 disji2 3996 tz7.2 4354 funopg 5250 fvun1 5582 fvopab6 5612 isores3 5815 ovmpt4g 5996 ovmpos 5997 ov2gf 5998 ofrval 6092 poxp 6232 smoel 6300 tfr1onlemaccex 6348 tfrcllemaccex 6361 nnaass 6485 qsel 6611 xpdom3m 6833 phpm 6864 ctssdc 7111 mkvprop 7155 prarloclem3 7495 aptisr 7777 axpre-apti 7883 axapti 8026 addn0nid 8329 divvalap 8629 letrp1 8803 p1le 8804 zextle 9342 zextlt 9343 btwnnz 9345 gtndiv 9346 uzind2 9363 fzind 9366 iccleub 9929 uzsubsubfz 10044 elfz0fzfz0 10123 difelfznle 10132 elfzo0le 10182 fzonmapblen 10184 fzofzim 10185 fzosplitprm1 10231 rebtwn2zlemstep 10250 qbtwnxr 10255 icogelb 10263 expcl2lemap 10529 expclzaplem 10541 expnegzap 10551 leexp2r 10571 expnbnd 10640 bcval4 10727 bccmpl 10729 absexpzap 11084 divalgb 11924 ndvdssub 11929 dvdsgcd 12007 dfgcd2 12009 rplpwr 12022 nnmindc 12029 lcmgcdlem 12071 coprmdvds1 12085 qredeq 12090 prmdvdsexpr 12144 nnnn0modprm0 12249 pcexp 12303 difsqpwdvds 12331 prmpwdvds 12347 elrestr 12690 isnmgm 12773 grpasscan1 12927 grpinvnz 12935 mulgneg2 13010 dvdsrmul1 13264 dvdsunit 13274 mopni 13913 sincosq1lem 14177 logbgcd1irr 14316 |
Copyright terms: Public domain | W3C validator |