| 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 1204 |
. 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 982 |
| This theorem is referenced by: 3anidm12 1307 mob 2954 eqbrrdva 4847 funimaexglem 5356 fco 5440 f1oiso2 5895 caovimo 6139 smoel2 6388 nnaword 6596 3ecoptocl 6710 rex2dom 6909 sbthlemi10 7067 distrnq0 7571 addassnq0 7574 prcdnql 7596 prcunqu 7597 genpdisj 7635 cauappcvgprlemrnd 7762 caucvgprlemrnd 7785 caucvgprprlemrnd 7813 nn0n0n1ge2b 9451 fzind 9487 icoshft 10111 fzen 10164 seq3coll 10985 shftuz 11099 mulgcd 12308 algcvga 12344 lcmneg 12367 isnmgm 13163 gsummgmpropd 13197 issgrpd 13215 iscmnd 13605 unitmulclb 13847 rmodislmodlem 14083 rmodislmod 14084 blssps 14870 blss 14871 metcnp3 14954 sincosq1sgn 15269 sincosq2sgn 15270 sincosq3sgn 15271 sincosq4sgn 15272 |
| Copyright terms: Public domain | W3C validator |