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: wi 4 wa 103 |
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 1745 funtp 5236 foimacnv 5445 respreima 5608 fpr 5662 dmtpos 6216 ixpsnf1o 6694 ssdomg 6736 exmidfodomrlemim 7149 archnqq 7350 recexgt0sr 7706 ige2m2fzo 10124 climeu 11227 algcvgblem 11970 qredeu 12018 qnumdencoprm 12114 qeqnumdivden 12115 eltg3i 12623 topbas 12634 neipsm 12721 lmbrf 12782 exmidsbthrlem 13763 |
Copyright terms: Public domain | W3C validator |