Metamath Proof Explorer


Theorem bj-nnfand

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 ) )

Proof

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 ) )