![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > jca | Structured version Visualization version GIF version |
Description: Deduce conjunction of the consequents of two implications ("join consequents with 'and'"). Deduction form of pm3.2 468 and pm3.2i 469. Its associated deduction is jcad 511. Equivalent to the natural deduction rule ∧ I (∧ introduction), see natded 30285. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2012.) |
Ref | Expression |
---|---|
jca.1 | ⊢ (𝜑 → 𝜓) |
jca.2 | ⊢ (𝜑 → 𝜒) |
Ref | Expression |
---|---|
jca | ⊢ (𝜑 → (𝜓 ∧ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | jca.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | jca.2 | . 2 ⊢ (𝜑 → 𝜒) | |
3 | pm3.2 468 | . 2 ⊢ (𝜓 → (𝜒 → (𝜓 ∧ 𝜒))) | |
4 | 1, 2, 3 | sylc 65 | 1 ⊢ (𝜑 → (𝜓 ∧ 𝜒)) |
Copyright terms: Public domain | W3C validator |