Theorem 3ax5VD 16686

Description: Virtual deduction proof of 3ax5 5832. 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::	|- . A.x(ph -> (ps -> ch))    ⊢   A.x(ph -> (ps -> ch)) .
2:1,?: e1_ 16518	|- . A.x(ph -> (ps -> ch))    ⊢   (A.xph -> A.x(ps -> ch)) .
3::	|- (A.x(ps -> ch) -> (A.xps -> A.xch))
4:2,3,?: e10 16585	|- . A.x(ph -> (ps -> ch))    ⊢   (A.xph -> (A.xps -> A.xch)) .
qed:4:	|- (A.x(ph -> (ps -> ch)) -> (A.xph -> (A.xps -> A.xch)))

Assertion

Ref	Expression
3ax5VD	|- (A.x(ph -> (ps -> ch)) -> (A.xph -> (A.xps -> A.xch)))

Proof of Theorem 3ax5VD

Step	Hyp	Ref	Expression
1		idn1 16484	. . . 4 |- . A.x(ph -> (ps -> ch))   ⊢   A.x(ph -> (ps -> ch)) .
2		ax-5 1302	. . . 4 |- (A.x(ph -> (ps -> ch)) -> (A.xph -> A.x(ps -> ch)))
3	1, 2	e1_ 16518	. . 3 |- . A.x(ph -> (ps -> ch))   ⊢   (A.xph -> A.x(ps -> ch)) .
4		ax-5 1302	. . 3 |- (A.x(ps -> ch) -> (A.xps -> A.xch))
5		imim1 18	. . 3 |- ((A.xph -> A.x(ps -> ch)) -> ((A.x(ps -> ch) -> (A.xps -> A.xch)) -> (A.xph -> (A.xps -> A.xch))))
6	3, 4, 5	e10 16585	. 2 |- . A.x(ph -> (ps -> ch))   ⊢   (A.xph -> (A.xps -> A.xch)) .
7	6	in1 16481	1 |- (A.x(ph -> (ps -> ch)) -> (A.xph -> (A.xps -> A.xch)))

Syntax hints:   -> wi 3  A.wal 1296

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1302

This theorem depends on definitions:  df-bi 164  df-vd1 16480

Copyright terms: Public domain