Homework Statement
I'm having some issues coming up with a proof for |- (Box(P) ^ Box(Q)) -> Box(P ^ Q).
Box is the unary operator for "necessary for".
Homework Equations
Axiom 1 A -> (B -> A)
Axiom 2 (A -> (B -> C)) -> ((A->B) -> (A -> C))
Axiom 3 (~a -> B) -> ((~A -> ~B) -> A)...