![]() |
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 300 | 1 ⊢ (𝜑 → (𝜓 ∧ 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia3 106 |
This theorem is referenced by: jctr 308 equvini 1685 funtp 5023 foimacnv 5222 respreima 5375 fpr 5424 dmtpos 5956 ssdomg 6428 exmidfodomrlemim 6748 archnqq 6897 recexgt0sr 7240 ige2m2fzo 9512 climeu 10523 algcvgblem 10825 qredeu 10873 qnumdencoprm 10965 qeqnumdivden 10966 exmidsbthrlem 11268 |
Copyright terms: Public domain | W3C validator |