Theorem 3impexpVD 16680

Description: Virtual deduction proof of 3impexp 1286. 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 /\ ps /\ ch) -> th)   ⊢   ((ph /\ ps /\ ch) -> th) .
2::	|- ((ph /\ ps /\ ch) <-> ((ph /\ ps) /\ ch))
3:1,2,?: e10 16585	|- . ((ph /\ ps /\ ch) -> th)   ⊢   (((ph /\ ps) /\ ch) -> th) .
4:3,?: e1_ 16518	|- . ((ph /\ ps /\ ch) -> th)   ⊢   ((ph /\ ps) -> (ch -> th)) .
5:4,?: e1_ 16518	|- . ((ph /\ ps /\ ch) -> th)   ⊢   (ph -> (ps -> (ch -> th))) .
6:5:	|- (((ph /\ ps /\ ch) -> th) -> (ph -> (ps -> (ch -> th))))
7::	|- . (ph -> (ps -> (ch -> th)))   ⊢   (ph -> (ps -> (ch -> th))) .
8:7,?: e1_ 16518	|- . (ph -> (ps -> (ch -> th)))   ⊢   ((ph /\ ps) -> (ch -> th)) .
9:8,?: e1_ 16518	|- . (ph -> (ps -> (ch -> th)))   ⊢   (((ph /\ ps) /\ ch) -> th) .
10:2,9,?: e01 16581	|- . (ph -> (ps -> (ch -> th)))   ⊢   ((ph /\ ps /\ ch) -> th) .
11:10:	|- ((ph -> (ps -> (ch -> th))) -> ((ph /\ ps /\ ch) -> th))
qed:6,11,?: e00 16635	|- (((ph /\ ps /\ ch) -> th) <-> (ph -> (ps -> (ch -> th))))

Assertion

Ref	Expression
3impexpVD	|- (((ph /\ ps /\ ch) -> th) <-> (ph -> (ps -> (ch -> th))))

Proof of Theorem 3impexpVD

Step	Hyp	Ref	Expression
1		idn1 16484	. . . . . 6 |- . ((ph /\ ps /\ ch) -> th)   ⊢   ((ph /\ ps /\ ch) -> th) .
2		df-3an 860	. . . . . 6 |- ((ph /\ ps /\ ch) <-> ((ph /\ ps) /\ ch))
3		imbi1 685	. . . . . . 7 |- (((ph /\ ps /\ ch) <-> ((ph /\ ps) /\ ch)) -> (((ph /\ ps /\ ch) -> th) <-> (((ph /\ ps) /\ ch) -> th)))
4	3	biimpcd 172	. . . . . 6 |- (((ph /\ ps /\ ch) -> th) -> (((ph /\ ps /\ ch) <-> ((ph /\ ps) /\ ch)) -> (((ph /\ ps) /\ ch) -> th)))
5	1, 2, 4	e10 16585	. . . . 5 |- . ((ph /\ ps /\ ch) -> th)   ⊢   (((ph /\ ps) /\ ch) -> th) .
6		pm3.3 375	. . . . 5 |- ((((ph /\ ps) /\ ch) -> th) -> ((ph /\ ps) -> (ch -> th)))
7	5, 6	e1_ 16518	. . . 4 |- . ((ph /\ ps /\ ch) -> th)   ⊢   ((ph /\ ps) -> (ch -> th)) .
8		pm3.3 375	. . . 4 |- (((ph /\ ps) -> (ch -> th)) -> (ph -> (ps -> (ch -> th))))
9	7, 8	e1_ 16518	. . 3 |- . ((ph /\ ps /\ ch) -> th)   ⊢   (ph -> (ps -> (ch -> th))) .
10	9	in1 16481	. 2 |- (((ph /\ ps /\ ch) -> th) -> (ph -> (ps -> (ch -> th))))
11		idn1 16484	. . . . . 6 |- . (ph -> (ps -> (ch -> th)))   ⊢   (ph -> (ps -> (ch -> th))) .
12		pm3.31 376	. . . . . 6 |- ((ph -> (ps -> (ch -> th))) -> ((ph /\ ps) -> (ch -> th)))
13	11, 12	e1_ 16518	. . . . 5 |- . (ph -> (ps -> (ch -> th)))   ⊢   ((ph /\ ps) -> (ch -> th)) .
14		pm3.31 376	. . . . 5 |- (((ph /\ ps) -> (ch -> th)) -> (((ph /\ ps) /\ ch) -> th))
15	13, 14	e1_ 16518	. . . 4 |- . (ph -> (ps -> (ch -> th)))   ⊢   (((ph /\ ps) /\ ch) -> th) .
16	3	biimprd 171	. . . 4 |- (((ph /\ ps /\ ch) <-> ((ph /\ ps) /\ ch)) -> ((((ph /\ ps) /\ ch) -> th) -> ((ph /\ ps /\ ch) -> th)))
17	2, 15, 16	e01 16581	. . 3 |- . (ph -> (ps -> (ch -> th)))   ⊢   ((ph /\ ps /\ ch) -> th) .
18	17	in1 16481	. 2 |- ((ph -> (ps -> (ch -> th))) -> ((ph /\ ps /\ ch) -> th))
19		bi3 167	. 2 |- ((((ph /\ ps /\ ch) -> th) -> (ph -> (ps -> (ch -> th)))) -> (((ph -> (ps -> (ch -> th))) -> ((ph /\ ps /\ ch) -> th)) -> (((ph /\ ps /\ ch) -> th) <-> (ph -> (ps -> (ch -> th))))))
20	10, 18, 19	e00 16635	1 |- (((ph /\ ps /\ ch) -> th) <-> (ph -> (ps -> (ch -> th))))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858

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

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

Copyright terms: Public domain