inference

proof.txt

https://www.umsu.de/trees/#((a%E2%86%92c)%E2%88%A7(b%E2%86%92d))%E2%86%92((a%E2%88%A7b)%E2%86%92(c%E2%88%A7d))

---

A -> C
B -> D
A & B
---
C & D

// conjunction elimination with A & B

A -> C
B -> D
A
B
---
C & D

// conditional elimination (modus ponens) with A and B

C
D
---
C & D

// conjunction introduction with C and D

C & D
---
C & D QED.