Description: Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 14-Oct-2010)
Ref | Expression | ||
---|---|---|---|
Hypotheses | jca3.1 | ⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) ) | |
jca3.2 | ⊢ ( 𝜃 → 𝜏 ) | ||
Assertion | jca3 | ⊢ ( 𝜑 → ( 𝜓 → ( 𝜃 → ( 𝜒 ∧ 𝜏 ) ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | jca3.1 | ⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) ) | |
2 | jca3.2 | ⊢ ( 𝜃 → 𝜏 ) | |
3 | 1 | imp | ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜒 ) |
4 | 3 | a1d | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝜃 → 𝜒 ) ) |
5 | 4 2 | jca2 | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝜃 → ( 𝜒 ∧ 𝜏 ) ) ) |
6 | 5 | ex | ⊢ ( 𝜑 → ( 𝜓 → ( 𝜃 → ( 𝜒 ∧ 𝜏 ) ) ) ) |