Theorem exbiriVD 16678

Description: Virtual deduction proof of exbiri 421. 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.

h1::	|- ((ph /\ ps) -> (ch <-> th))
2::	|- . ph   ⊢   ph .
3::	|- . ph, ps   ⊢   ps .
4::	|- . ph, ps, th   ⊢   th .
5:2,1,?: e10 16585	|- . ph   ⊢   (ps -> (ch <-> th)) .
6:3,5,?: e21 16598	|- . ph, ps   ⊢   (ch <-> th) .
7:4,6,?: e32 16626	|- . ph, ps, th   ⊢   ch .
8:7:	|- . ph, ps   ⊢   (th -> ch) .
9:8:	|- . ph   ⊢   (ps -> (th -> ch)) .
qed:9:	|- (ph -> (ps -> (th -> ch)))

Hypothesis

Ref	Expression
exbiriVD.1	|- ((ph /\ ps) -> (ch <-> th))

Assertion

Ref	Expression
exbiriVD	|- (ph -> (ps -> (th -> ch)))

Proof of Theorem exbiriVD

Step	Hyp	Ref	Expression
1		idn3 16510	. . . . 5 |- . ph, ps, th   ⊢   th .
2		idn2 16509	. . . . . 6 |- . ph, ps   ⊢   ps .
3		idn1 16484	. . . . . . 7 |- . ph   ⊢   ph .
4		exbiriVD.1	. . . . . . 7 |- ((ph /\ ps) -> (ch <-> th))
5		pm3.3 375	. . . . . . . 8 |- (((ph /\ ps) -> (ch <-> th)) -> (ph -> (ps -> (ch <-> th))))
6	5	com12 14	. . . . . . 7 |- (ph -> (((ph /\ ps) -> (ch <-> th)) -> (ps -> (ch <-> th))))
7	3, 4, 6	e10 16585	. . . . . 6 |- . ph   ⊢   (ps -> (ch <-> th)) .
8		pm2.27 76	. . . . . 6 |- (ps -> ((ps -> (ch <-> th)) -> (ch <-> th)))
9	2, 7, 8	e21 16598	. . . . 5 |- . ph, ps   ⊢   (ch <-> th) .
10		bi2 166	. . . . . 6 |- ((ch <-> th) -> (th -> ch))
11	10	com12 14	. . . . 5 |- (th -> ((ch <-> th) -> ch))
12	1, 9, 11	e32 16626	. . . 4 |- . ph, ps, th   ⊢   ch .
13	12	in3 16508	. . 3 |- . ph, ps   ⊢   (th -> ch) .
14	13	in2 16506	. 2 |- . ph   ⊢   (ps -> (th -> ch)) .
15	14	in1 16481	1 |- (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