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 | ⊢ ( ∀ 𝑥 ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( ∀ 𝑥 𝜑 → ( ∀ 𝑥 𝜓 → ∀ 𝑥 𝜒 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | idn1 | ⊢ ( ∀ 𝑥 ( 𝜑 → ( 𝜓 → 𝜒 ) ) ▶ ∀ 𝑥 ( 𝜑 → ( 𝜓 → 𝜒 ) ) ) | |
2 | alim | ⊢ ( ∀ 𝑥 ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( ∀ 𝑥 𝜑 → ∀ 𝑥 ( 𝜓 → 𝜒 ) ) ) | |
3 | 1 2 | e1a | ⊢ ( ∀ 𝑥 ( 𝜑 → ( 𝜓 → 𝜒 ) ) ▶ ( ∀ 𝑥 𝜑 → ∀ 𝑥 ( 𝜓 → 𝜒 ) ) ) |
4 | alim | ⊢ ( ∀ 𝑥 ( 𝜓 → 𝜒 ) → ( ∀ 𝑥 𝜓 → ∀ 𝑥 𝜒 ) ) | |
5 | imim1 | ⊢ ( ( ∀ 𝑥 𝜑 → ∀ 𝑥 ( 𝜓 → 𝜒 ) ) → ( ( ∀ 𝑥 ( 𝜓 → 𝜒 ) → ( ∀ 𝑥 𝜓 → ∀ 𝑥 𝜒 ) ) → ( ∀ 𝑥 𝜑 → ( ∀ 𝑥 𝜓 → ∀ 𝑥 𝜒 ) ) ) ) | |
6 | 3 4 5 | e10 | ⊢ ( ∀ 𝑥 ( 𝜑 → ( 𝜓 → 𝜒 ) ) ▶ ( ∀ 𝑥 𝜑 → ( ∀ 𝑥 𝜓 → ∀ 𝑥 𝜒 ) ) ) |
7 | 6 | in1 | ⊢ ( ∀ 𝑥 ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( ∀ 𝑥 𝜑 → ( ∀ 𝑥 𝜓 → ∀ 𝑥 𝜒 ) ) ) |