Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE 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 887 | . 2 | |
2 | 3imp.1 | . . 3 | |
3 | 2 | imp31 243 | . 2 |
4 | 1, 3 | sylbi 114 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 97 w3a 885 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 |
This theorem depends on definitions: df-bi 110 df-3an 887 |
This theorem is referenced by: 3impa 1099 3impb 1100 3impia 1101 3impib 1102 3com23 1110 3an1rs 1116 3imp1 1117 3impd 1118 syl3an2 1169 syl3an3 1170 3jao 1196 biimp3ar 1236 poxp 5853 tfrlemibxssdm 5941 nndi 6065 nnmass 6066 difelfzle 8992 fzo1fzo0n0 9039 elfzo0z 9040 fzofzim 9044 elfzodifsumelfzo 9057 mulexp 9294 expadd 9297 expmul 9300 bernneq 9369 |
Copyright terms: Public domain | W3C validator |