![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > jctir | GIF 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: → wi 4 ∧ wa 104 |
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 1768 funtp 5281 foimacnv 5491 respreima 5657 fpr 5711 dmtpos 6270 ixpsnf1o 6749 ssdomg 6791 exmidfodomrlemim 7213 archnqq 7429 recexgt0sr 7785 ige2m2fzo 10211 climeu 11317 algcvgblem 12062 qredeu 12110 qnumdencoprm 12206 qeqnumdivden 12207 eltg3i 13827 topbas 13838 neipsm 13925 lmbrf 13986 exmidsbthrlem 15042 |
Copyright terms: Public domain | W3C validator |