Theorem exbiriVD 39089

Description: Virtual deduction proof of exbiri 652. 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 38919	|- (. ph ->. ( ps -> ( ch <-> th ) ) ).
6:3,5,?: e21 38957	|- (. ph ,. ps ->. ( ch <-> th ) ).
7:4,6,?: e32 38985	|- (. ph ,. ps ,. th ->. ch ).
8:7:	|- (. ph ,. ps ->. ( th -> ch ) ).
9:8:	|- (. ph ->. ( ps -> ( th -> ch ) ) ).
qed:9:	|- ( ph -> ( ps -> ( th -> ch ) ) )

(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

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 38840	. . . . 5 |- (. ph ,. ps ,. th ->. th ).
2		idn2 38838	. . . . . 6 |- (. ph ,. ps ->. ps ).
3		idn1 38790	. . . . . . 7 |- (. ph ->. ph ).
4		exbiriVD.1	. . . . . . 7 |- ( ( ph /\ ps ) -> ( ch <-> th ) )
5		pm3.3 460	. . . . . . . 8 |- ( ( ( ph /\ ps ) -> ( ch <-> th ) ) -> ( ph -> ( ps -> ( ch <-> th ) ) ) )
6	5	com12 32	. . . . . . 7 |- ( ph -> ( ( ( ph /\ ps ) -> ( ch <-> th ) ) -> ( ps -> ( ch <-> th ) ) ) )
7	3, 4, 6	e10 38919	. . . . . 6 |- (. ph ->. ( ps -> ( ch <-> th ) ) ).
8		pm2.27 42	. . . . . 6 |- ( ps -> ( ( ps -> ( ch <-> th ) ) -> ( ch <-> th ) ) )
9	2, 7, 8	e21 38957	. . . . 5 |- (. ph ,. ps ->. ( ch <-> th ) ).
10		biimpr 210	. . . . . 6 |- ( ( ch <-> th ) -> ( th -> ch ) )
11	10	com12 32	. . . . 5 |- ( th -> ( ( ch <-> th ) -> ch ) )
12	1, 9, 11	e32 38985	. . . 4 |- (. ph ,. ps ,. th ->. ch ).
13	12	in3 38834	. . 3 |- (. ph ,. ps ->. ( th -> ch ) ).
14	13	in2 38830	. 2 |- (. ph ->. ( ps -> ( th -> ch ) ) ).
15	14	in1 38787	1 |- ( ph -> ( ps -> ( th -> ch ) ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384

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

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039  df-vd1 38786  df-vd2 38794  df-vd3 38806

This theorem is referenced by: (None)