Description: Nonfreeness in both conjuncts implies nonfreeness in the conjunction,
deduction form. Note: compared with the proof of bj-nnfan , it has
two more essential steps but fewer total steps (since there are fewer
intermediate formulas to build) and is easier to follow and understand.
This statement is of intermediate complexity: for simpler statements,
closed-style proofs like that of bj-nnfan will generally be shorter
than deduction-style proofs while still easy to follow, while for more
complex statements, the opposite will be true (and deduction-style
proofs like that of bj-nnfand will generally be easier to understand).
(Contributed by BJ, 19-Nov-2023)(Proof modification is discouraged.)