Theorem bj-nnford

Description: Nonfreeness in both disjuncts implies nonfreeness in the disjunction, deduction form. See comments for bj-nnfor and bj-nnfand . (Contributed by BJ, 2-Dec-2023) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	bj-nnford.1	|- ( ph -> F// x ps )
	bj-nnford.2	|- ( ph -> F// x ch )
Assertion	bj-nnford	|- ( ph -> F// x ( ps \/ ch ) )

Proof

Step	Hyp	Ref	Expression
1		bj-nnford.1	|- ( ph -> F// x ps )
2		bj-nnford.2	|- ( ph -> F// x ch )
3		19.43	|- ( 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	orim12d	|- ( ph -> ( ( E. x ps \/ E. x ch ) -> ( ps \/ ch ) ) )
7	3 6	biimtrid	|- ( 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	orim12d	|- ( ph -> ( ( ps \/ ch ) -> ( A. x ps \/ A. x ch ) ) )
11		19.33	|- ( ( A. x ps \/ A. x ch ) -> A. x ( ps \/ ch ) )
12	10 11	syl6	|- ( 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 ) )