Theorem 19.21a3con13vVD 39087

Description: Virtual deduction proof of alrim3con13v 38743. 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.

1::	|- (. ( ph -> A. x ph ) ->. ( ph -> A. x ph ) ).
2::	|- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. ( ps /\ ph /\ ch ) ).
3:2,?: e2 38856	|- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. ps ).
4:2,?: e2 38856	|- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. ph ).
5:2,?: e2 38856	|- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. ch ).
6:1,4,?: e12 38951	|- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. A. x ph ).
7:3,?: e2 38856	|- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. A. x ps ).
8:5,?: e2 38856	|- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. A. x ch ).
9:7,6,8,?: e222 38861	|- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. ( A. x ps /\ A. x ph /\ A. x ch ) ).
10:9,?: e2 38856	|- (. ( 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 ) ) )

(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
19.21a3con13vVD	|- ( ( ph -> A. x ph ) -> ( ( ps /\ ph /\ ch ) -> A. x ( ps /\ ph /\ ch ) ) )

Distinct variable groups:   ps, x   ch, x

Allowed substitution hint:   ph( x)

Proof of Theorem 19.21a3con13vVD

Step	Hyp	Ref	Expression
1		idn2 38838	. . . . . . 7 |- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. ( ps /\ ph /\ ch ) ).
2		simp1 1061	. . . . . . 7 |- ( ( ps /\ ph /\ ch ) -> ps )
3	1, 2	e2 38856	. . . . . 6 |- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. ps ).
4		ax-5 1839	. . . . . 6 |- ( ps -> A. x ps )
5	3, 4	e2 38856	. . . . 5 |- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. A. x ps ).
6		idn1 38790	. . . . . 6 |- (. ( ph -> A. x ph ) ->. ( ph -> A. x ph ) ).
7		simp2 1062	. . . . . . 7 |- ( ( ps /\ ph /\ ch ) -> ph )
8	1, 7	e2 38856	. . . . . 6 |- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. ph ).
9		id 22	. . . . . 6 |- ( ( ph -> A. x ph ) -> ( ph -> A. x ph ) )
10	6, 8, 9	e12 38951	. . . . 5 |- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. A. x ph ).
11		simp3 1063	. . . . . . 7 |- ( ( ps /\ ph /\ ch ) -> ch )
12	1, 11	e2 38856	. . . . . 6 |- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. ch ).
13		ax-5 1839	. . . . . 6 |- ( ch -> A. x ch )
14	12, 13	e2 38856	. . . . 5 |- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. A. x ch ).
15		pm3.2an3 1240	. . . . 5 |- ( A. x ps -> ( A. x ph -> ( A. x ch -> ( A. x ps /\ A. x ph /\ A. x ch ) ) ) )
16	5, 10, 14, 15	e222 38861	. . . 4 |- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. ( A. x ps /\ A. x ph /\ A. x ch ) ).
17		19.26-3an 1800	. . . . 5 |- ( A. x ( ps /\ ph /\ ch ) <-> ( A. x ps /\ A. x ph /\ A. x ch ) )
18	17	biimpri 218	. . . 4 |- ( ( A. x ps /\ A. x ph /\ A. x ch ) -> A. x ( ps /\ ph /\ ch ) )
19	16, 18	e2 38856	. . 3 |- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. A. x ( ps /\ ph /\ ch ) ).
20	19	in2 38830	. 2 |- (. ( ph -> A. x ph ) ->. ( ( ps /\ ph /\ ch ) -> A. x ( ps /\ ph /\ ch ) ) ).
21	20	in1 38787	1 |- ( ( ph -> A. x ph ) -> ( ( ps /\ ph /\ ch ) -> A. x ( ps /\ ph /\ ch ) ) )

Syntax hints:   -> wi 4   /\ w3a 1037   A.wal 1481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039  df-vd1 38786  df-vd2 38794

This theorem is referenced by: (None)