![]() |
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 463 and pm3.2i 464. Its associated deduction is jcad 508. Equivalent to the natural deduction rule ∧ I (∧ introduction), see natded 27835. (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 463 | . 2 ⊢ (𝜓 → (𝜒 → (𝜓 ∧ 𝜒))) | |
4 | 1, 2, 3 | sylc 65 | 1 ⊢ (𝜑 → (𝜓 ∧ 𝜒)) |
Copyright terms: Public domain | W3C validator |