Metamath Proof Explorer

Theorem hb3an

Description: If x is not free in ph , ps , and ch , it is not free in ( ph /\ ps /\ ch ) . (Contributed by NM, 14-Sep-2003) (Proof shortened by Wolf Lammen, 2-Jan-2018) Reduce axiom dependencies. (Revised by SN and Sky Winter, 23-Oct-2026)

Ref Expression
Hypotheses hb.1 ⊢ φ → ∀ x φ
hb.2 ⊢ ψ → ∀ x ψ
hb.3 ⊢ χ → ∀ x χ
Assertion hb3an ⊢ φ ∧ ψ ∧ χ → ∀ x φ ∧ ψ ∧ χ

Proof

Step Hyp Ref Expression
1 hb.1 ⊢ φ → ∀ x φ
2 hb.2 ⊢ ψ → ∀ x ψ
3 hb.3 ⊢ χ → ∀ x χ
4 df-3an ⊢ φ ∧ ψ ∧ χ ↔ φ ∧ ψ ∧ χ
5 1 2 hban ⊢ φ ∧ ψ → ∀ x φ ∧ ψ
6 5 3 hban ⊢ φ ∧ ψ ∧ χ → ∀ x φ ∧ ψ ∧ χ
7 4 6 hbxfrbi ⊢ φ ∧ ψ ∧ χ → ∀ x φ ∧ ψ ∧ χ