| 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 1205 |
. 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 983 |
| This theorem is referenced by: 3anidm12 1308 mob 2955 eqbrrdva 4848 funimaexglem 5357 fco 5441 f1oiso2 5896 caovimo 6140 smoel2 6389 nnaword 6597 3ecoptocl 6711 rex2dom 6910 sbthlemi10 7068 distrnq0 7572 addassnq0 7575 prcdnql 7597 prcunqu 7598 genpdisj 7636 cauappcvgprlemrnd 7763 caucvgprlemrnd 7786 caucvgprprlemrnd 7814 nn0n0n1ge2b 9452 fzind 9488 icoshft 10112 fzen 10165 seq3coll 10987 shftuz 11128 mulgcd 12337 algcvga 12373 lcmneg 12396 isnmgm 13192 gsummgmpropd 13226 issgrpd 13244 iscmnd 13634 unitmulclb 13876 rmodislmodlem 14112 rmodislmod 14113 blssps 14899 blss 14900 metcnp3 14983 sincosq1sgn 15298 sincosq2sgn 15299 sincosq3sgn 15300 sincosq4sgn 15301 |
| Copyright terms: Public domain | W3C validator |