Description: Virtual deduction proof of 3impexpbicomi . 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,?: e0a | |- ( ph -> ( ps -> ( ch -> ( ta <-> th ) ) ) ) |
Ref | Expression | ||
---|---|---|---|
Hypothesis | 3impexpbicomiVD.1 | |- ( ( ph /\ ps /\ ch ) -> ( th <-> ta ) ) |
|
Assertion | 3impexpbicomiVD | |- ( ph -> ( ps -> ( ch -> ( ta <-> th ) ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3impexpbicomiVD.1 | |- ( ( ph /\ ps /\ ch ) -> ( th <-> ta ) ) |
|
2 | 3impexpbicom | |- ( ( ( ph /\ ps /\ ch ) -> ( th <-> ta ) ) <-> ( ph -> ( ps -> ( ch -> ( ta <-> th ) ) ) ) ) |
|
3 | 2 | biimpi | |- ( ( ( ph /\ ps /\ ch ) -> ( th <-> ta ) ) -> ( ph -> ( ps -> ( ch -> ( ta <-> th ) ) ) ) ) |
4 | 1 3 | e0a | |- ( ph -> ( ps -> ( ch -> ( ta <-> th ) ) ) ) |