Theorem 19.21a3con13vVD 16676

Description: Virtual deduction proof of 19.21a3con13v 5828. 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.xph)    ⊢   (ph -> A.xph) .
2::	|- . (ph -> A.xph), (ps /\ ph /\ ch)   ⊢   (ps /\ ph /\ ch) .
3:2,?: e2 16521	|- . (ph -> A.xph), (ps /\ ph /\ ch)   ⊢   ps .
4:2,?: e2 16521	|- . (ph -> A.xph), (ps /\ ph /\ ch)   ⊢   ph .
5:2,?: e2 16521	|- . (ph -> A.xph), (ps /\ ph /\ ch)   ⊢   ch .
6:1,4,?: e12 16593	|- . (ph -> A.xph), (ps /\ ph /\ ch)   ⊢   A.xph .
7:3,?: e2 16521	|- . (ph -> A.xph), (ps /\ ph /\ ch)   ⊢   A.xps .
8:5,?: e2 16521	|- . (ph -> A.xph), (ps /\ ph /\ ch)   ⊢   A.xch .
9:7,6,8,?: e222 16526	|- . (ph -> A.xph), (ps /\ ph /\ ch)   ⊢   (A.xps /\ A.xph /\ A.xch) .
10:9,?: e2 16521	|- . (ph -> A.xph), (ps /\ ph /\ ch)   ⊢   A.x(ps /\ ph /\ ch) .
11:10:in2	|- . (ph -> A.xph)   ⊢   ((ps /\ ph /\ ch) -> A.x(ps /\ ph /\ ch)) .
qed:11:in1	|- ((ph -> A.xph) -> ((ps /\ ph /\ ch) -> A.x(ps /\ ph /\ ch)))

Assertion

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

Distinct variable groups:   ps,x   ch,x

Proof of Theorem 19.21a3con13vVD

Step	Hyp	Ref	Expression
1		idn2 16509	. . . . . . 7 |- . (ph -> A.xph), (ps /\ ph /\ ch)   ⊢   (ps /\ ph /\ ch) .
2		simp1 876	. . . . . . 7 |- ((ps /\ ph /\ ch) -> ps)
3	1, 2	e2 16521	. . . . . 6 |- . (ph -> A.xph), (ps /\ ph /\ ch)   ⊢   ps .
4		ax-17 1317	. . . . . 6 |- (ps -> A.xps)
5	3, 4	e2 16521	. . . . 5 |- . (ph -> A.xph), (ps /\ ph /\ ch)   ⊢   A.xps .
6		idn1 16484	. . . . . 6 |- . (ph -> A.xph)   ⊢   (ph -> A.xph) .
7		simp2 877	. . . . . . 7 |- ((ps /\ ph /\ ch) -> ph)
8	1, 7	e2 16521	. . . . . 6 |- . (ph -> A.xph), (ps /\ ph /\ ch)   ⊢   ph .
9		id 73	. . . . . 6 |- ((ph -> A.xph) -> (ph -> A.xph))
10	6, 8, 9	e12 16593	. . . . 5 |- . (ph -> A.xph), (ps /\ ph /\ ch)   ⊢   A.xph .
11		simp3 878	. . . . . . 7 |- ((ps /\ ph /\ ch) -> ch)
12	1, 11	e2 16521	. . . . . 6 |- . (ph -> A.xph), (ps /\ ph /\ ch)   ⊢   ch .
13		ax-17 1317	. . . . . 6 |- (ch -> A.xch)
14	12, 13	e2 16521	. . . . 5 |- . (ph -> A.xph), (ps /\ ph /\ ch)   ⊢   A.xch .
15		pm3.2an3 1049	. . . . 5 |- (A.xps -> (A.xph -> (A.xch -> (A.xps /\ A.xph /\ A.xch))))
16	5, 10, 14, 15	e222 16526	. . . 4 |- . (ph -> A.xph), (ps /\ ph /\ ch)   ⊢   (A.xps /\ A.xph /\ A.xch) .
17		19.26-3an 1418	. . . . 5 |- (A.x(ps /\ ph /\ ch) <-> (A.xps /\ A.xph /\ A.xch))
18	17	biimpri 169	. . . 4 |- ((A.xps /\ A.xph /\ A.xch) -> A.x(ps /\ ph /\ ch))
19	16, 18	e2 16521	. . 3 |- . (ph -> A.xph), (ps /\ ph /\ ch)   ⊢   A.x(ps /\ ph /\ ch) .
20	19	in2 16506	. 2 |- . (ph -> A.xph)   ⊢   ((ps /\ ph /\ ch) -> A.x(ps /\ ph /\ ch)) .
21	20	in1 16481	1 |- ((ph -> A.xph) -> ((ps /\ ph /\ ch) -> A.x(ps /\ ph /\ ch)))

Syntax hints:   -> wi 3   /\ w3a 858  A.wal 1296

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321

This theorem depends on definitions:  df-bi 164  df-an 242  df-3an 860  df-vd1 16480  df-vd2 16489

Copyright terms: Public domain