![]() |
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 886 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 3imp.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | imp31 243 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | sylbi 114 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
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 886 |
This theorem is referenced by: 3impa 1098 3impb 1099 3impia 1100 3impib 1101 3com23 1109 3an1rs 1115 3imp1 1116 3impd 1117 syl3an2 1168 syl3an3 1169 3jao 1195 biimp3ar 1235 poxp 5794 tfrlemibxssdm 5882 nndi 6004 nnmass 6005 difelfzle 8762 fzo1fzo0n0 8809 elfzo0z 8810 fzofzim 8814 elfzodifsumelfzo 8827 mulexp 8948 expadd 8951 expmul 8954 bernneq 9022 |
Copyright terms: Public domain | W3C validator |