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 1218 euan 2062 imadiflem 5249 supelti 6946 ltexnqq 7328 enq0sym 7352 enq0tr 7354 addclpr 7457 mulclpr 7492 ltexprlemopl 7521 ltexprlemlol 7522 ltexprlemopu 7523 ltexprlemupu 7524 suplocexprlemloc 7641 lemul12a 8733 fzass4 9964 elfz1b 9992 4fvwrd4 10039 leexp1a 10474 sqrt0rlem 10903 reumodprminv 12128 uptx 12685 distspace 12746 xmetxpbl 12919 bj-charfundc 13394 |
Copyright terms: Public domain | W3C validator |