![]() |
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 306 | . 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃)) |
5 | 1, 4 | jca 306 | 1 ⊢ (𝜑 → (𝜓 ∧ (𝜒 ∧ 𝜃))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 108 |
This theorem is referenced by: syl12anc 1236 euan 2082 imadiflem 5294 supelti 6998 ltexnqq 7404 enq0sym 7428 enq0tr 7430 addclpr 7533 mulclpr 7568 ltexprlemopl 7597 ltexprlemlol 7598 ltexprlemopu 7599 ltexprlemupu 7600 suplocexprlemloc 7717 lemul12a 8815 fzass4 10057 elfz1b 10085 4fvwrd4 10135 leexp1a 10570 sqrt0rlem 11005 reumodprminv 12245 uptx 13645 distspace 13706 xmetxpbl 13879 bj-charfundc 14420 |
Copyright terms: Public domain | W3C validator |