![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > jca32 | GIF version |
Description: Join three consequents. (Contributed by FL, 1-Aug-2009.) |
Ref | Expression |
---|---|
jca31.1 | ⊢ (𝜑 → 𝜓) |
jca31.2 | ⊢ (𝜑 → 𝜒) |
jca31.3 | ⊢ (𝜑 → 𝜃) |
Ref | Expression |
---|---|
jca32 | ⊢ (𝜑 → (𝜓 ∧ (𝜒 ∧ 𝜃))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | jca31.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | jca31.2 | . . 3 ⊢ (𝜑 → 𝜒) | |
3 | jca31.3 | . . 3 ⊢ (𝜑 → 𝜃) | |
4 | 2, 3 | jca 290 | . 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃)) |
5 | 1, 4 | jca 290 | 1 ⊢ (𝜑 → (𝜓 ∧ (𝜒 ∧ 𝜃))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia3 101 |
This theorem is referenced by: syl12anc 1133 euan 1956 imadiflem 4978 ltexnqq 6506 enq0sym 6530 enq0tr 6532 addclpr 6635 mulclpr 6670 ltexprlemopl 6699 ltexprlemlol 6700 ltexprlemopu 6701 ltexprlemupu 6702 lemul12a 7828 fzass4 8925 elfz1b 8952 4fvwrd4 8997 leexp1a 9309 sqrt0rlem 9601 |
Copyright terms: Public domain | W3C validator |