Description: Join three consequents. (Contributed by FL, 1-Aug-2009)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | jca31.1 | ⊢ ( 𝜑 → 𝜓 ) | |
| jca31.2 | ⊢ ( 𝜑 → 𝜒 ) | ||
| jca31.3 | ⊢ ( 𝜑 → 𝜃 ) | ||
| Assertion | jca32 | ⊢ ( 𝜑 → ( 𝜓 ∧ ( 𝜒 ∧ 𝜃 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | jca31.1 | ⊢ ( 𝜑 → 𝜓 ) | |
| 2 | jca31.2 | ⊢ ( 𝜑 → 𝜒 ) | |
| 3 | jca31.3 | ⊢ ( 𝜑 → 𝜃 ) | |
| 4 | 2 3 | jca | ⊢ ( 𝜑 → ( 𝜒 ∧ 𝜃 ) ) |
| 5 | 1 4 | jca | ⊢ ( 𝜑 → ( 𝜓 ∧ ( 𝜒 ∧ 𝜃 ) ) ) |