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 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 1716 funtp 5146 foimacnv 5353 respreima 5516 fpr 5570 dmtpos 6121 ixpsnf1o 6598 ssdomg 6640 exmidfodomrlemim 7025 archnqq 7193 recexgt0sr 7549 ige2m2fzo 9943 climeu 11033 algcvgblem 11657 qredeu 11705 qnumdencoprm 11798 qeqnumdivden 11799 eltg3i 12152 topbas 12163 neipsm 12250 lmbrf 12311 exmidsbthrlem 13144 |
Copyright terms: Public domain | W3C validator |