Metamath Proof Explorer

Theorem alrim3con13v

Description: Closed form of alrimi with 2 additional conjuncts having no occurrences of the quantifying variable. This proof is 19.21a3con13vVD automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion alrim3con13v ⊢ φ → ∀ x φ → ψ ∧ φ ∧ χ → ∀ x ψ ∧ φ ∧ χ

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ψ ∧ φ ∧ χ → ψ
2 1 a1i ⊢ φ → ∀ x φ → ψ ∧ φ ∧ χ → ψ
3 ax-5 ⊢ ψ → ∀ x ψ
4 2 3 syl6 ⊢ φ → ∀ x φ → ψ ∧ φ ∧ χ → ∀ x ψ
5 simp2 ⊢ ψ ∧ φ ∧ χ → φ
6 5 imim1i ⊢ φ → ∀ x φ → ψ ∧ φ ∧ χ → ∀ x φ
7 simp3 ⊢ ψ ∧ φ ∧ χ → χ
8 7 a1i ⊢ φ → ∀ x φ → ψ ∧ φ ∧ χ → χ
9 ax-5 ⊢ χ → ∀ x χ
10 8 9 syl6 ⊢ φ → ∀ x φ → ψ ∧ φ ∧ χ → ∀ x χ
11 4 6 10 3jcad ⊢ φ → ∀ x φ → ψ ∧ φ ∧ χ → ∀ x ψ ∧ ∀ x φ ∧ ∀ x χ
12 19.26-3an ⊢ ∀ x ψ ∧ φ ∧ χ ↔ ∀ x ψ ∧ ∀ x φ ∧ ∀ x χ
13 11 12 imbitrrdi ⊢ φ → ∀ x φ → ψ ∧ φ ∧ χ → ∀ x ψ ∧ φ ∧ χ