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 5721 nnnq0lem1 7247 prmuloc 7367 suplocexprlemex 7523 prsrlem1 7543 apreap 8342 lemulge11 8617 elnnz 9057 supinfneg 9383 infsupneg 9384 leexp1a 10341 faclbnd6 10483 zfz1isolem1 10576 oddpwdclemdc 11840 ennnfonelemf1 11920 cncnp2m 12389 |
Copyright terms: Public domain | W3C validator |