Theorem 3impexpbicomiVD 16682

Description: Virtual deduction proof of 3impexpbicomi 1288. 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 <-> ta))
qed:1,?: e0_ 16637	|- (ph -> (ps -> (ch -> (ta <-> th))))

Hypothesis

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

Assertion

Ref	Expression
3impexpbicomiVD	|- (ph -> (ps -> (ch -> (ta <-> th))))

Proof of Theorem 3impexpbicomiVD

Step	Hyp	Ref	Expression
1		3impexpbicomiVD.1	. 2 |- ((ph /\ ps /\ ch) -> (th <-> ta))
2		3impexpbicom 1287	. . 3 |- (((ph /\ ps /\ ch) -> (th <-> ta)) <-> (ph -> (ps -> (ch -> (ta <-> th)))))
3	2	biimpi 168	. 2 |- (((ph /\ ps /\ ch) -> (th <-> ta)) -> (ph -> (ps -> (ch -> (ta <-> th)))))
4	1, 3	e0_ 16637	1 |- (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

Copyright terms: Public domain