Description: Virtual deduction proof of al2im . 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:: | |- (. A. x ( ph -> ( ps -> ch ) ) ->. A. x ( ph -> ( ps -> ch ) ) ). |
2:1,?: e1a | |- (. A. x ( ph -> ( ps -> ch ) ) ->. ( A. x ph -> A. x ( ps -> ch ) ) ). |
3:: | |- ( A. x ( ps -> ch ) -> ( A. x ps -> A. x ch ) ) |
4:2,3,?: e10 | |- (. A. x ( ph -> ( ps -> ch ) ) ->. ( A. x ph -> ( A. x ps -> A. x ch ) ) ). |
qed:4: | |- ( A. x ( ph -> ( ps -> ch ) ) -> ( A. x ph -> ( A. x ps -> A. x ch ) ) ) |
Ref | Expression | ||
---|---|---|---|
Assertion | al2imVD | |- ( A. x ( ph -> ( ps -> ch ) ) -> ( A. x ph -> ( A. x ps -> A. x ch ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | idn1 | |- (. A. x ( ph -> ( ps -> ch ) ) ->. A. x ( ph -> ( ps -> ch ) ) ). |
|
2 | alim | |- ( A. x ( ph -> ( ps -> ch ) ) -> ( A. x ph -> A. x ( ps -> ch ) ) ) |
|
3 | 1 2 | e1a | |- (. A. x ( ph -> ( ps -> ch ) ) ->. ( A. x ph -> A. x ( ps -> ch ) ) ). |
4 | alim | |- ( A. x ( ps -> ch ) -> ( A. x ps -> A. x ch ) ) |
|
5 | imim1 | |- ( ( A. x ph -> A. x ( ps -> ch ) ) -> ( ( A. x ( ps -> ch ) -> ( A. x ps -> A. x ch ) ) -> ( A. x ph -> ( A. x ps -> A. x ch ) ) ) ) |
|
6 | 3 4 5 | e10 | |- (. A. x ( ph -> ( ps -> ch ) ) ->. ( A. x ph -> ( A. x ps -> A. x ch ) ) ). |
7 | 6 | in1 | |- ( A. x ( ph -> ( ps -> ch ) ) -> ( A. x ph -> ( A. x ps -> A. x ch ) ) ) |