![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3impa | Unicode version |
Description: Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.) |
Ref | Expression |
---|---|
3impa.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3impa |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3impa.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | exp31 357 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | 3imp 1138 |
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 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 927 |
This theorem is referenced by: 3impdir 1231 syl3an9b 1247 biimp3a 1282 stoic3 1366 rspec3 2464 rspc3v 2738 raltpg 3499 rextpg 3500 disjiun 3846 otexg 4066 opelopabt 4098 tpexg 4279 3optocl 4529 fun2ssres 5070 funssfv 5343 fvun1 5383 foco2 5547 f1elima 5566 eloprabga 5749 caovimo 5852 ot1stg 5937 ot2ndg 5938 ot3rdgg 5939 brtposg 6033 rdgexggg 6156 rdgivallem 6160 nnmass 6262 nndir 6265 nnaword 6284 th3q 6411 ecovass 6415 ecoviass 6416 fpmg 6445 findcard 6658 unfiin 6690 addasspig 6950 mulasspig 6952 mulcanpig 6955 ltapig 6958 ltmpig 6959 addassnqg 7002 ltbtwnnqq 7035 mulnnnq0 7070 addassnq0 7082 genpassl 7144 genpassu 7145 genpassg 7146 aptiprleml 7259 adddir 7540 le2tri3i 7654 addsub12 7756 subdir 7925 reapmul1 8133 recexaplem2 8182 div12ap 8222 divdiv32ap 8248 divdivap1 8251 lble 8469 zaddcllemneg 8850 fnn0ind 8923 xrltso 9327 iccgelb 9411 elicc4 9419 elfz 9491 fzrevral 9580 expnegap0 10024 expgt0 10049 expge0 10052 expge1 10053 mulexpzap 10056 expp1zap 10065 expm1ap 10066 abssubap0 10584 binom 10939 dvds0lem 11145 dvdsnegb 11152 muldvds1 11160 muldvds2 11161 divalgmodcl 11267 gcd2n0cl 11300 lcmdvds 11400 prmdvdsexp 11466 rpexp1i 11472 |
Copyright terms: Public domain | W3C validator |