Theorem 3impexpbicomVD 16681

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

Assertion

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

Proof of Theorem 3impexpbicomVD

Step	Hyp	Ref	Expression
1		idn1 16484	. . . . 5 |- . ((ph /\ ps /\ ch) -> (th <-> ta))   ⊢   ((ph /\ ps /\ ch) -> (th <-> ta)) .
2		bicom 579	. . . . 5 |- ((th <-> ta) <-> (ta <-> th))
3		imbi2 686	. . . . . 6 |- (((th <-> ta) <-> (ta <-> th)) -> (((ph /\ ps /\ ch) -> (th <-> ta)) <-> ((ph /\ ps /\ ch) -> (ta <-> th))))
4	3	biimpcd 172	. . . . 5 |- (((ph /\ ps /\ ch) -> (th <-> ta)) -> (((th <-> ta) <-> (ta <-> th)) -> ((ph /\ ps /\ ch) -> (ta <-> th))))
5	1, 2, 4	e10 16585	. . . 4 |- . ((ph /\ ps /\ ch) -> (th <-> ta))   ⊢   ((ph /\ ps /\ ch) -> (ta <-> th)) .
6		3impexp 1286	. . . . 5 |- (((ph /\ ps /\ ch) -> (ta <-> th)) <-> (ph -> (ps -> (ch -> (ta <-> th)))))
7	6	biimpi 168	. . . 4 |- (((ph /\ ps /\ ch) -> (ta <-> th)) -> (ph -> (ps -> (ch -> (ta <-> th)))))
8	5, 7	e1_ 16518	. . 3 |- . ((ph /\ ps /\ ch) -> (th <-> ta))   ⊢   (ph -> (ps -> (ch -> (ta <-> th)))) .
9	8	in1 16481	. 2 |- (((ph /\ ps /\ ch) -> (th <-> ta)) -> (ph -> (ps -> (ch -> (ta <-> th)))))
10		idn1 16484	. . . . 5 |- . (ph -> (ps -> (ch -> (ta <-> th))))   ⊢   (ph -> (ps -> (ch -> (ta <-> th)))) .
11	6	biimpri 169	. . . . 5 |- ((ph -> (ps -> (ch -> (ta <-> th)))) -> ((ph /\ ps /\ ch) -> (ta <-> th)))
12	10, 11	e1_ 16518	. . . 4 |- . (ph -> (ps -> (ch -> (ta <-> th))))   ⊢   ((ph /\ ps /\ ch) -> (ta <-> th)) .
13	3	biimprcd 173	. . . 4 |- (((ph /\ ps /\ ch) -> (ta <-> th)) -> (((th <-> ta) <-> (ta <-> th)) -> ((ph /\ ps /\ ch) -> (th <-> ta))))
14	12, 2, 13	e10 16585	. . 3 |- . (ph -> (ps -> (ch -> (ta <-> th))))   ⊢   ((ph /\ ps /\ ch) -> (th <-> ta)) .
15	14	in1 16481	. 2 |- ((ph -> (ps -> (ch -> (ta <-> th)))) -> ((ph /\ ps /\ ch) -> (th <-> ta)))
16		bi3 167	. 2 |- ((((ph /\ ps /\ ch) -> (th <-> ta)) -> (ph -> (ps -> (ch -> (ta <-> th))))) -> (((ph -> (ps -> (ch -> (ta <-> th)))) -> ((ph /\ ps /\ ch) -> (th <-> ta))) -> (((ph /\ ps /\ ch) -> (th <-> ta)) <-> (ph -> (ps -> (ch -> (ta <-> th)))))))
17	9, 15, 16	e00 16635	1 |- (((ph /\ ps /\ ch) -> (th <-> ta)) <-> (ph -> (ps -> (ch -> (ta <-> th)))))

Syntax hints:   -> wi 3   <-> wb 163   /\ 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