The andL proof rule expresses that if we have a conjunction P∧Q among our assumptions, then we can separately assume both conjuncts P as well as Q, instead.

See also