Theorem exbirVD 16677

Description: Virtual deduction proof of exbir 1285. 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 <-> th)), (ph /\ ps)   ⊢   (ph /\ ps) .
3::	|- . ((ph /\ ps) -> (ch <-> th)), (ph /\ ps), th   ⊢   th .
5:1,2,?: e12 16593	|- . ((ph /\ ps) -> (ch <-> th)), (ph /\ ps)   ⊢   (ch <-> th) .
6:3,5,?: e32 16626	|- . ((ph /\ ps) -> (ch <-> th)), (ph /\ ps), th   ⊢   ch .
7:6:	|- . ((ph /\ ps) -> (ch <-> th)), (ph /\ ps)   ⊢   (th -> ch) .
8:7:	|- . ((ph /\ ps) -> (ch <-> th))    ⊢   ((ph /\ ps) -> (th -> ch)) .
9:8,?: e1_ 16518	|- . ((ph /\ ps) -> (ch <-> th))   ⊢   (ph -> (ps -> (th -> ch))) .
qed:9:	|- (((ph /\ ps) -> (ch <-> th)) -> (ph -> (ps -> (th -> ch))))

Assertion

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

Proof of Theorem exbirVD

Step	Hyp	Ref	Expression
1		idn3 16510	. . . . . 6 |- . ((ph /\ ps) -> (ch <-> th)), (ph /\ ps), th   ⊢   th .
2		idn1 16484	. . . . . . 7 |- . ((ph /\ ps) -> (ch <-> th))   ⊢   ((ph /\ ps) -> (ch <-> th)) .
3		idn2 16509	. . . . . . 7 |- . ((ph /\ ps) -> (ch <-> th)), (ph /\ ps)   ⊢   (ph /\ ps) .
4		id 73	. . . . . . 7 |- (((ph /\ ps) -> (ch <-> th)) -> ((ph /\ ps) -> (ch <-> th)))
5	2, 3, 4	e12 16593	. . . . . 6 |- . ((ph /\ ps) -> (ch <-> th)), (ph /\ ps)   ⊢   (ch <-> th) .
6		bi2 166	. . . . . . 7 |- ((ch <-> th) -> (th -> ch))
7	6	com12 14	. . . . . 6 |- (th -> ((ch <-> th) -> ch))
8	1, 5, 7	e32 16626	. . . . 5 |- . ((ph /\ ps) -> (ch <-> th)), (ph /\ ps), th   ⊢   ch .
9	8	in3 16508	. . . 4 |- . ((ph /\ ps) -> (ch <-> th)), (ph /\ ps)   ⊢   (th -> ch) .
10	9	in2 16506	. . 3 |- . ((ph /\ ps) -> (ch <-> th))   ⊢   ((ph /\ ps) -> (th -> ch)) .
11		pm3.3 375	. . 3 |- (((ph /\ ps) -> (th -> ch)) -> (ph -> (ps -> (th -> ch))))
12	10, 11	e1_ 16518	. 2 |- . ((ph /\ ps) -> (ch <-> th))   ⊢   (ph -> (ps -> (th -> ch))) .
13	12	in1 16481	1 |- (((ph /\ ps) -> (ch <-> th)) -> (ph -> (ps -> (th -> ch))))

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

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  df-vd2 16489  df-vd3 16494

Copyright terms: Public domain