Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > jca31 | GIF version |
Description: Join three consequents. (Contributed by Jeff Hankins, 1-Aug-2009.) |
Ref | Expression |
---|---|
jca31.1 | ⊢ (𝜑 → 𝜓) |
jca31.2 | ⊢ (𝜑 → 𝜒) |
jca31.3 | ⊢ (𝜑 → 𝜃) |
Ref | Expression |
---|---|
jca31 | ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | jca31.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | jca31.2 | . . 3 ⊢ (𝜑 → 𝜒) | |
3 | 1, 2 | jca 304 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒)) |
4 | jca31.3 | . 2 ⊢ (𝜑 → 𝜃) | |
5 | 3, 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: 3jca 1161 syl21anc 1215 f1oiso2 5728 nnnq0lem1 7254 prmuloc 7374 suplocexprlemex 7530 prsrlem1 7550 apreap 8349 lemulge11 8624 elnnz 9064 supinfneg 9390 infsupneg 9391 leexp1a 10348 faclbnd6 10490 zfz1isolem1 10583 oddpwdclemdc 11851 ennnfonelemf1 11931 cncnp2m 12400 |
Copyright terms: Public domain | W3C validator |