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 1731 funtp 5176 foimacnv 5385 respreima 5548 fpr 5602 dmtpos 6153 ixpsnf1o 6630 ssdomg 6672 exmidfodomrlemim 7057 archnqq 7225 recexgt0sr 7581 ige2m2fzo 9975 climeu 11065 algcvgblem 11730 qredeu 11778 qnumdencoprm 11871 qeqnumdivden 11872 eltg3i 12225 topbas 12236 neipsm 12323 lmbrf 12384 exmidsbthrlem 13217 |
Copyright terms: Public domain | W3C validator |