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 1214 euan 2055 imadiflem 5202 supelti 6889 ltexnqq 7216 enq0sym 7240 enq0tr 7242 addclpr 7345 mulclpr 7380 ltexprlemopl 7409 ltexprlemlol 7410 ltexprlemopu 7411 ltexprlemupu 7412 suplocexprlemloc 7529 lemul12a 8620 fzass4 9842 elfz1b 9870 4fvwrd4 9917 leexp1a 10348 sqrt0rlem 10775 uptx 12443 distspace 12504 xmetxpbl 12677 |
Copyright terms: Public domain | W3C validator |