![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > jctir | Unicode version |
Description: Inference conjoining a theorem to right of consequent in an implication. (Contributed by NM, 31-Dec-1993.) |
Ref | Expression |
---|---|
jctil.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
jctil.2 |
![]() ![]() |
Ref | Expression |
---|---|
jctir |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | jctil.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | jctil.2 |
. . 3
![]() ![]() | |
3 | 2 | a1i 9 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | jca 304 |
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-ia3 107 |
This theorem is referenced by: jctr 313 equvini 1732 funtp 5184 foimacnv 5393 respreima 5556 fpr 5610 dmtpos 6161 ixpsnf1o 6638 ssdomg 6680 exmidfodomrlemim 7074 archnqq 7249 recexgt0sr 7605 ige2m2fzo 10006 climeu 11097 algcvgblem 11766 qredeu 11814 qnumdencoprm 11907 qeqnumdivden 11908 eltg3i 12264 topbas 12275 neipsm 12362 lmbrf 12423 exmidsbthrlem 13392 |
Copyright terms: Public domain | W3C validator |