New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > 3imp | Unicode version |
Description: Importation inference. (Contributed by NM, 8-Apr-1994.) |
Ref | Expression |
---|---|
3imp.1 |
Ref | Expression |
---|---|
3imp |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-3an 936 | . 2 | |
2 | 3imp.1 | . . 3 | |
3 | 2 | imp31 421 | . 2 |
4 | 1, 3 | sylbi 187 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 358 w3a 934 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 177 df-an 360 df-3an 936 |
This theorem is referenced by: 3impa 1146 3impb 1147 3impia 1148 3impib 1149 3com23 1157 3an1rs 1163 3imp1 1164 3impd 1165 syl3an2 1216 syl3an3 1217 3jao 1243 biimp3ar 1282 ltfintri 4466 ssfin 4470 nnadjoin 4520 sfintfin 4532 tfinnn 4534 nclenn 6249 |
Copyright terms: Public domain | W3C validator |