![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3expib | Unicode version |
Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.) |
Ref | Expression |
---|---|
3exp.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3expib |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3exp.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | 3exp 1202 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | impd 254 |
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: 3anidm12 1295 mob 2919 eqbrrdva 4797 funimaexglem 5299 fco 5381 f1oiso2 5827 caovimo 6067 smoel2 6303 nnaword 6511 3ecoptocl 6623 sbthlemi10 6964 distrnq0 7457 addassnq0 7460 prcdnql 7482 prcunqu 7483 genpdisj 7521 cauappcvgprlemrnd 7648 caucvgprlemrnd 7671 caucvgprprlemrnd 7699 nn0n0n1ge2b 9330 fzind 9366 icoshft 9988 fzen 10040 seq3coll 10817 shftuz 10821 mulgcd 12011 algcvga 12045 lcmneg 12068 isnmgm 12733 iscmnd 13054 unitmulclb 13236 blssps 13820 blss 13821 metcnp3 13904 sincosq1sgn 14140 sincosq2sgn 14141 sincosq3sgn 14142 sincosq4sgn 14143 |
Copyright terms: Public domain | W3C validator |