RISC JKU
Distributivity of ForAll over Implication

(da) [Graphics:indexgr19.gif]

with no assumptions.

We prove (da) by natural deduction.

We prove (da) in both directions.

Direction from left to right:

Direction from right to left: