New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > 3exp | Unicode version |
Description: Exportation inference. (Contributed by NM, 30-May-1994.) |
Ref | Expression |
---|---|
3exp.1 |
Ref | Expression |
---|---|
3exp |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm3.2an3 1131 | . 2 | |
2 | 3exp.1 | . 2 | |
3 | 1, 2 | syl8 65 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 w3a 934 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 |
This theorem depends on definitions: df-bi 177 df-an 360 df-3an 936 |
This theorem is referenced by: 3expa 1151 3expb 1152 3expia 1153 3expib 1154 3com23 1157 3an1rs 1163 3exp1 1167 3expd 1168 exp5o 1170 syl3an2 1216 syl3an3 1217 3ecase 1286 3impexpbicomi 1368 rexlimdv3a 2740 rabssdv 3346 reupick2 3541 ssfin 4470 tfin11 4493 f1oiso2 5500 funsi 5520 trrd 5925 nchoicelem17 6305 |
Copyright terms: Public domain | W3C validator |