This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database SUPPLEMENTARY MATERIAL (USERS' MATHBOXES) Mathbox for BJ First-order logic Nonfreeness bj-nnfimd
Description: Nonfreeness in the antecedent and the consequent of an implication
implies nonfreeness in the implication, deduction form. (Contributed by BJ , 2-Dec-2023)
Ref
Expression
Hypotheses
bj-nnfimd.1 ⊢ ( 𝜑 → Ⅎ' 𝑥 𝜓 )
bj-nnfimd.2 ⊢ ( 𝜑 → Ⅎ' 𝑥 𝜒 )
Assertion
bj-nnfimd ⊢ ( 𝜑 → Ⅎ' 𝑥 ( 𝜓 → 𝜒 ) )
Proof
Step
Hyp
Ref
Expression
1
bj-nnfimd.1 ⊢ ( 𝜑 → Ⅎ' 𝑥 𝜓 )
2
bj-nnfimd.2 ⊢ ( 𝜑 → Ⅎ' 𝑥 𝜒 )
3
bj-nnfim ⊢ ( ( Ⅎ' 𝑥 𝜓 ∧ Ⅎ' 𝑥 𝜒 ) → Ⅎ' 𝑥 ( 𝜓 → 𝜒 ) )
4
1 2 3
syl2anc ⊢ ( 𝜑 → Ⅎ' 𝑥 ( 𝜓 → 𝜒 ) )