![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3impb | Unicode version |
Description: Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.) |
Ref | Expression |
---|---|
3impb.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3impb |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3impb.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | exp32 365 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | 3imp 1194 |
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 981 |
This theorem is referenced by: 3adant1l 1231 3adant1r 1232 3impdi 1303 vtocl3gf 2812 rspc2ev 2868 reuss 3428 trssord 4392 funtp 5281 resdif 5495 funimass4 5579 fnovex 5921 fnotovb 5931 fovcdm 6030 fnovrn 6035 fmpoco 6230 nndi 6500 nnaordi 6522 ecovass 6657 ecoviass 6658 ecovdi 6659 ecovidi 6660 eqsupti 7008 addasspig 7342 mulasspig 7344 distrpig 7345 distrnq0 7471 addassnq0 7474 distnq0r 7475 prcdnql 7496 prcunqu 7497 genpassl 7536 genpassu 7537 genpassg 7538 distrlem1prl 7594 distrlem1pru 7595 ltexprlemopl 7613 ltexprlemopu 7615 le2tri3i 8079 cnegexlem1 8145 subadd 8173 addsub 8181 subdi 8355 submul2 8369 div12ap 8664 diveqap1 8675 divnegap 8676 divdivap2 8694 ltmulgt11 8834 gt0div 8840 ge0div 8841 uzind3 9379 fnn0ind 9382 qdivcl 9656 irrmul 9660 xrlttr 9808 fzen 10056 lenegsq 11117 moddvds 11819 dvds2add 11845 dvds2sub 11846 dvdsleabs 11864 divalgb 11943 ndvdsadd 11949 modgcd 12005 absmulgcd 12031 odzval 12254 pcmul 12314 setsresg 12513 issubmnd 12864 submcl 12891 grpinvid1 12948 grpinvid2 12949 mulgp1 13047 cmncom 13138 islss3 13563 unopn 13776 innei 13934 cncfi 14336 |
Copyright terms: Public domain | W3C validator |