This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ ( 𝜑 → Ⅎ' 𝑥 𝜓 )
		bj-nnford.2	⊢ ( 𝜑 → Ⅎ' 𝑥 𝜒 )
	Assertion	bj-nnford	⊢ ( 𝜑 → Ⅎ' 𝑥 ( 𝜓 ∨ 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		bj-nnford.1	⊢ ( 𝜑 → Ⅎ' 𝑥 𝜓 )
2		bj-nnford.2	⊢ ( 𝜑 → Ⅎ' 𝑥 𝜒 )
3		19.43	⊢ ( ∃ 𝑥 ( 𝜓 ∨ 𝜒 ) ↔ ( ∃ 𝑥 𝜓 ∨ ∃ 𝑥 𝜒 ) )
4	1	bj-nnfed	⊢ ( 𝜑 → ( ∃ 𝑥 𝜓 → 𝜓 ) )
5	2	bj-nnfed	⊢ ( 𝜑 → ( ∃ 𝑥 𝜒 → 𝜒 ) )
6	4 5	orim12d	⊢ ( 𝜑 → ( ( ∃ 𝑥 𝜓 ∨ ∃ 𝑥 𝜒 ) → ( 𝜓 ∨ 𝜒 ) ) )
7	3 6	biimtrid	⊢ ( 𝜑 → ( ∃ 𝑥 ( 𝜓 ∨ 𝜒 ) → ( 𝜓 ∨ 𝜒 ) ) )
8	1	bj-nnfad	⊢ ( 𝜑 → ( 𝜓 → ∀ 𝑥 𝜓 ) )
9	2	bj-nnfad	⊢ ( 𝜑 → ( 𝜒 → ∀ 𝑥 𝜒 ) )
10	8 9	orim12d	⊢ ( 𝜑 → ( ( 𝜓 ∨ 𝜒 ) → ( ∀ 𝑥 𝜓 ∨ ∀ 𝑥 𝜒 ) ) )
11		19.33	⊢ ( ( ∀ 𝑥 𝜓 ∨ ∀ 𝑥 𝜒 ) → ∀ 𝑥 ( 𝜓 ∨ 𝜒 ) )
12	10 11	syl6	⊢ ( 𝜑 → ( ( 𝜓 ∨ 𝜒 ) → ∀ 𝑥 ( 𝜓 ∨ 𝜒 ) ) )
13		df-bj-nnf	⊢ ( Ⅎ' 𝑥 ( 𝜓 ∨ 𝜒 ) ↔ ( ( ∃ 𝑥 ( 𝜓 ∨ 𝜒 ) → ( 𝜓 ∨ 𝜒 ) ) ∧ ( ( 𝜓 ∨ 𝜒 ) → ∀ 𝑥 ( 𝜓 ∨ 𝜒 ) ) ) )
14	7 12 13	sylanbrc	⊢ ( 𝜑 → Ⅎ' 𝑥 ( 𝜓 ∨ 𝜒 ) )