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 304 | . 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃)) |
5 | 1, 4 | 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: syl12anc 1199 euan 2033 imadiflem 5172 supelti 6857 ltexnqq 7184 enq0sym 7208 enq0tr 7210 addclpr 7313 mulclpr 7348 ltexprlemopl 7377 ltexprlemlol 7378 ltexprlemopu 7379 ltexprlemupu 7380 suplocexprlemloc 7497 lemul12a 8584 fzass4 9797 elfz1b 9825 4fvwrd4 9872 leexp1a 10303 sqrt0rlem 10730 uptx 12354 distspace 12415 xmetxpbl 12588 |
Copyright terms: Public domain | W3C validator |