![]() |
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 1181 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | impd 252 |
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 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 965 |
This theorem is referenced by: 3anidm12 1274 mob 2870 eqbrrdva 4717 funimaexglem 5214 fco 5296 f1oiso2 5736 caovimo 5972 smoel2 6208 nnaword 6415 3ecoptocl 6526 sbthlemi10 6862 distrnq0 7291 addassnq0 7294 prcdnql 7316 prcunqu 7317 genpdisj 7355 cauappcvgprlemrnd 7482 caucvgprlemrnd 7505 caucvgprprlemrnd 7533 nn0n0n1ge2b 9154 fzind 9190 icoshft 9803 fzen 9854 seq3coll 10617 shftuz 10621 mulgcd 11740 algcvga 11768 lcmneg 11791 blssps 12635 blss 12636 metcnp3 12719 sincosq1sgn 12955 sincosq2sgn 12956 sincosq3sgn 12957 sincosq4sgn 12958 |
Copyright terms: Public domain | W3C validator |