![]() |
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 5269 foimacnv 5479 respreima 5644 fpr 5698 dmtpos 6256 ixpsnf1o 6735 ssdomg 6777 exmidfodomrlemim 7199 archnqq 7415 recexgt0sr 7771 ige2m2fzo 10197 climeu 11303 algcvgblem 12048 qredeu 12096 qnumdencoprm 12192 qeqnumdivden 12193 eltg3i 13526 topbas 13537 neipsm 13624 lmbrf 13685 exmidsbthrlem 14740 |
Copyright terms: Public domain | W3C validator |