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	⊢ ( ( 𝜑 → ∀ 𝑥 𝜑 ) → ( ( 𝜓 ∧ 𝜑 ∧ 𝜒 ) → ∀ 𝑥 ( 𝜓 ∧ 𝜑 ∧ 𝜒 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝜓 ∧ 𝜑 ∧ 𝜒 ) → 𝜓 )
2	1	a1i	⊢ ( ( 𝜑 → ∀ 𝑥 𝜑 ) → ( ( 𝜓 ∧ 𝜑 ∧ 𝜒 ) → 𝜓 ) )
3		ax-5	⊢ ( 𝜓 → ∀ 𝑥 𝜓 )
4	2 3	syl6	⊢ ( ( 𝜑 → ∀ 𝑥 𝜑 ) → ( ( 𝜓 ∧ 𝜑 ∧ 𝜒 ) → ∀ 𝑥 𝜓 ) )
5		simp2	⊢ ( ( 𝜓 ∧ 𝜑 ∧ 𝜒 ) → 𝜑 )
6	5	imim1i	⊢ ( ( 𝜑 → ∀ 𝑥 𝜑 ) → ( ( 𝜓 ∧ 𝜑 ∧ 𝜒 ) → ∀ 𝑥 𝜑 ) )
7		simp3	⊢ ( ( 𝜓 ∧ 𝜑 ∧ 𝜒 ) → 𝜒 )
8	7	a1i	⊢ ( ( 𝜑 → ∀ 𝑥 𝜑 ) → ( ( 𝜓 ∧ 𝜑 ∧ 𝜒 ) → 𝜒 ) )
9		ax-5	⊢ ( 𝜒 → ∀ 𝑥 𝜒 )
10	8 9	syl6	⊢ ( ( 𝜑 → ∀ 𝑥 𝜑 ) → ( ( 𝜓 ∧ 𝜑 ∧ 𝜒 ) → ∀ 𝑥 𝜒 ) )
11	4 6 10	3jcad	⊢ ( ( 𝜑 → ∀ 𝑥 𝜑 ) → ( ( 𝜓 ∧ 𝜑 ∧ 𝜒 ) → ( ∀ 𝑥 𝜓 ∧ ∀ 𝑥 𝜑 ∧ ∀ 𝑥 𝜒 ) ) )
12		19.26-3an	⊢ ( ∀ 𝑥 ( 𝜓 ∧ 𝜑 ∧ 𝜒 ) ↔ ( ∀ 𝑥 𝜓 ∧ ∀ 𝑥 𝜑 ∧ ∀ 𝑥 𝜒 ) )
13	11 12	imbitrrdi	⊢ ( ( 𝜑 → ∀ 𝑥 𝜑 ) → ( ( 𝜓 ∧ 𝜑 ∧ 𝜒 ) → ∀ 𝑥 ( 𝜓 ∧ 𝜑 ∧ 𝜒 ) ) )