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	$⊢ (φ \to \forall x φ) \to ((ψ \land φ \land χ) \to \forall x (ψ \land φ \land χ))$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (ψ \land φ \land χ) \to ψ$
2	1	a1i	$⊢ (φ \to \forall x φ) \to ((ψ \land φ \land χ) \to ψ)$
3		ax-5	$⊢ ψ \to \forall x ψ$
4	2 3	syl6	$⊢ (φ \to \forall x φ) \to ((ψ \land φ \land χ) \to \forall x ψ)$
5		simp2	$⊢ (ψ \land φ \land χ) \to φ$
6	5	imim1i	$⊢ (φ \to \forall x φ) \to ((ψ \land φ \land χ) \to \forall x φ)$
7		simp3	$⊢ (ψ \land φ \land χ) \to χ$
8	7	a1i	$⊢ (φ \to \forall x φ) \to ((ψ \land φ \land χ) \to χ)$
9		ax-5	$⊢ χ \to \forall x χ$
10	8 9	syl6	$⊢ (φ \to \forall x φ) \to ((ψ \land φ \land χ) \to \forall x χ)$
11	4 6 10	3jcad	$⊢ (φ \to \forall x φ) \to ((ψ \land φ \land χ) \to (\forall x ψ \land \forall x φ \land \forall x χ))$
12		19.26-3an	$⊢ \forall x (ψ \land φ \land χ) \leftrightarrow (\forall x ψ \land \forall x φ \land \forall x χ)$
13	11 12	imbitrrdi	$⊢ (φ \to \forall x φ) \to ((ψ \land φ \land χ) \to \forall x (ψ \land φ \land χ))$

Metamath Proof Explorer

Theorem alrim3con13v

Proof