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.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | bj-nnfand.1 | |- ( ph -> F// x ps ) |
|
bj-nnfand.2 | |- ( ph -> F// x ch ) |
||
Assertion | bj-nnfand | |- ( ph -> F// x ( ps /\ ch ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-nnfand.1 | |- ( ph -> F// x ps ) |
|
2 | bj-nnfand.2 | |- ( ph -> F// x ch ) |
|
3 | 19.40 | |- ( E. x ( ps /\ ch ) -> ( E. x ps /\ E. x ch ) ) |
|
4 | 1 | bj-nnfed | |- ( ph -> ( E. x ps -> ps ) ) |
5 | 2 | bj-nnfed | |- ( ph -> ( E. x ch -> ch ) ) |
6 | 4 5 | anim12d | |- ( ph -> ( ( E. x ps /\ E. x ch ) -> ( ps /\ ch ) ) ) |
7 | 3 6 | syl5 | |- ( ph -> ( E. x ( ps /\ ch ) -> ( ps /\ ch ) ) ) |
8 | 1 | bj-nnfad | |- ( ph -> ( ps -> A. x ps ) ) |
9 | 2 | bj-nnfad | |- ( ph -> ( ch -> A. x ch ) ) |
10 | 8 9 | anim12d | |- ( ph -> ( ( ps /\ ch ) -> ( A. x ps /\ A. x ch ) ) ) |
11 | 19.26 | |- ( A. x ( ps /\ ch ) <-> ( A. x ps /\ A. x ch ) ) |
|
12 | 10 11 | syl6ibr | |- ( ph -> ( ( ps /\ ch ) -> A. x ( ps /\ ch ) ) ) |
13 | df-bj-nnf | |- ( F// x ( ps /\ ch ) <-> ( ( E. x ( ps /\ ch ) -> ( ps /\ ch ) ) /\ ( ( ps /\ ch ) -> A. x ( ps /\ ch ) ) ) ) |
|
14 | 7 12 13 | sylanbrc | |- ( ph -> F// x ( ps /\ ch ) ) |