![]() |
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 306 |
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 108 |
This theorem is referenced by: jctr 315 equvini 1758 funtp 5270 foimacnv 5480 respreima 5645 fpr 5699 dmtpos 6257 ixpsnf1o 6736 ssdomg 6778 exmidfodomrlemim 7200 archnqq 7416 recexgt0sr 7772 ige2m2fzo 10198 climeu 11304 algcvgblem 12049 qredeu 12097 qnumdencoprm 12193 qeqnumdivden 12194 eltg3i 13559 topbas 13570 neipsm 13657 lmbrf 13718 exmidsbthrlem 14773 |
Copyright terms: Public domain | W3C validator |