![]() |
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 306 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒)) |
4 | jca31.3 | . 2 ⊢ (𝜑 → 𝜃) | |
5 | 3, 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: 3jca 1179 syl21anbrc 1184 syl21anc 1248 f1oiso2 5844 exmidapne 7277 nnnq0lem1 7463 prmuloc 7583 suplocexprlemex 7739 prsrlem1 7759 apreap 8562 lemulge11 8841 elnnz 9281 supinfneg 9613 infsupneg 9614 leexp1a 10593 faclbnd6 10742 zfz1isolem1 10838 oddpwdclemdc 12191 ennnfonelemf1 12437 grpidinv2 12968 rhmopp 13487 dvdsrzring 13863 cncnp2m 14115 bj-charfun 14943 |
Copyright terms: Public domain | W3C validator |