19.21a3con13vVD

Description: Virtual deduction proof of alrim3con13v . The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

		Ref	Expression
	Assertion	19.21a3con13vVD	$⊢ (φ \to \forall x φ) \to ((ψ \land φ \land χ) \to \forall x (ψ \land φ \land χ))$

Proof

Step	Hyp	Ref	Expression
1		idn2	$⊢ ((φ \to \forall x φ), (ψ \land φ \land χ) \to (ψ \land φ \land χ))$
2		simp1	$⊢ (ψ \land φ \land χ) \to ψ$
3	1 2	e2	$⊢ ((φ \to \forall x φ), (ψ \land φ \land χ) \to ψ)$
4		ax-5	$⊢ ψ \to \forall x ψ$
5	3 4	e2	$⊢ ((φ \to \forall x φ), (ψ \land φ \land χ) \to \forall x ψ)$
6		idn1	$⊢ ((φ \to \forall x φ) \to (φ \to \forall x φ))$
7		simp2	$⊢ (ψ \land φ \land χ) \to φ$
8	1 7	e2	$⊢ ((φ \to \forall x φ), (ψ \land φ \land χ) \to φ)$
9		id	$⊢ (φ \to \forall x φ) \to (φ \to \forall x φ)$
10	6 8 9	e12	$⊢ ((φ \to \forall x φ), (ψ \land φ \land χ) \to \forall x φ)$
11		simp3	$⊢ (ψ \land φ \land χ) \to χ$
12	1 11	e2	$⊢ ((φ \to \forall x φ), (ψ \land φ \land χ) \to χ)$
13		ax-5	$⊢ χ \to \forall x χ$
14	12 13	e2	$⊢ ((φ \to \forall x φ), (ψ \land φ \land χ) \to \forall x χ)$
15		pm3.2an3	$⊢ \forall x ψ \to (\forall x φ \to (\forall x χ \to (\forall x ψ \land \forall x φ \land \forall x χ)))$
16	5 10 14 15	e222	$⊢ ((φ \to \forall x φ), (ψ \land φ \land χ) \to (\forall x ψ \land \forall x φ \land \forall x χ))$
17		19.26-3an	$⊢ \forall x (ψ \land φ \land χ) \leftrightarrow (\forall x ψ \land \forall x φ \land \forall x χ)$
18	17	biimpri	$⊢ (\forall x ψ \land \forall x φ \land \forall x χ) \to \forall x (ψ \land φ \land χ)$
19	16 18	e2	$⊢ ((φ \to \forall x φ), (ψ \land φ \land χ) \to \forall x (ψ \land φ \land χ))$
20	19	in2	$⊢ ((φ \to \forall x φ) \to ((ψ \land φ \land χ) \to \forall x (ψ \land φ \land χ)))$
21	20	in1	$⊢ (φ \to \forall x φ) \to ((ψ \land φ \land χ) \to \forall x (ψ \land φ \land χ))$

1::	\|- (. ( ph -> A. x ph ) ->. ( ph -> A. x ph ) ).
2::	\|- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. ( ps /\ ph /\ ch ) ).
3:2,?: e2	\|- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. ps ).
4:2,?: e2	\|- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. ph ).
5:2,?: e2	\|- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. ch ).
6:1,4,?: e12	\|- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. A. x ph ).
7:3,?: e2	\|- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. A. x ps ).
8:5,?: e2	\|- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. A. x ch ).
9:7,6,8,?: e222	\|- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. ( A. x ps /\ A. x ph /\ A. x ch ) ).
10:9,?: e2	\|- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. A. x ( ps /\ ph /\ ch ) ).
11:10:in2	\|- (. ( ph -> A. x ph ) ->. ( ( ps /\ ph /\ ch ) -> A. x ( ps /\ ph /\ ch ) ) ).
qed:11:in1	\|- ( ( ph -> A. x ph ) -> ( ( ps /\ ph /\ ch ) -> A. x ( ps /\ ph /\ ch ) ) )

Metamath Proof Explorer

Theorem 19.21a3con13vVD

Proof