![]() |
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 1162 syl21anc 1216 f1oiso2 5736 nnnq0lem1 7278 prmuloc 7398 suplocexprlemex 7554 prsrlem1 7574 apreap 8373 lemulge11 8648 elnnz 9088 supinfneg 9417 infsupneg 9418 leexp1a 10379 faclbnd6 10522 zfz1isolem1 10615 oddpwdclemdc 11887 ennnfonelemf1 11967 cncnp2m 12439 |
Copyright terms: Public domain | W3C validator |