Metamath Proof Explorer

Theorem 19.21a3con13vVD

Description: Virtual deduction proof of alrim3con13v . 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 -> A. x ph ) ->. ( ph -> A. x ph ) ).
2:: |- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. ( ps /\ ph /\ ch ) ).
3:2,?: e2 |- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. ps ).
4:2,?: e2 |- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. ph ).
5:2,?: e2 |- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. ch ).
6:1,4,?: e12 |- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. A. x ph ).
7:3,?: e2 |- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. A. x ps ).
8:5,?: e2 |- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. A. x ch ).
9:7,6,8,?: e222 |- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. ( A. x ps /\ A. x ph /\ A. x ch ) ).
10:9,?: e2 |- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. A. x ( ps /\ ph /\ ch ) ).
11:10:in2 |- (. ( ph -> A. x ph ) ->. ( ( ps /\ ph /\ ch ) -> A. x ( ps /\ ph /\ ch ) ) ).
qed:11:in1 |- ( ( ph -> A. x ph ) -> ( ( ps /\ ph /\ ch ) -> A. x ( ps /\ ph /\ ch ) ) )
(Contributed by Alan Sare, 31-Dec-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion 19.21a3con13vVD ⊢φ→∀xφ→ψ∧φ∧χ→∀xψ∧φ∧χ

Proof

Step Hyp Ref Expression
1 idn2 ⊢φ→∀xφ,ψ∧φ∧χ→ψ∧φ∧χ
2 simp1 ⊢ψ∧φ∧χ→ψ
3 1 2 e2 ⊢φ→∀xφ,ψ∧φ∧χ→ψ
4 ax-5 ⊢ψ→∀xψ
5 3 4 e2 ⊢φ→∀xφ,ψ∧φ∧χ→∀xψ
6 idn1 ⊢φ→∀xφ→φ→∀xφ
7 simp2 ⊢ψ∧φ∧χ→φ
8 1 7 e2 ⊢φ→∀xφ,ψ∧φ∧χ→φ
9 id ⊢φ→∀xφ→φ→∀xφ
10 6 8 9 e12 ⊢φ→∀xφ,ψ∧φ∧χ→∀xφ
11 simp3 ⊢ψ∧φ∧χ→χ
12 1 11 e2 ⊢φ→∀xφ,ψ∧φ∧χ→χ
13 ax-5 ⊢χ→∀xχ
14 12 13 e2 ⊢φ→∀xφ,ψ∧φ∧χ→∀xχ
15 pm3.2an3 ⊢∀xψ→∀xφ→∀xχ→∀xψ∧∀xφ∧∀xχ
16 5 10 14 15 e222 ⊢φ→∀xφ,ψ∧φ∧χ→∀xψ∧∀xφ∧∀xχ
17 19.26-3an ⊢∀xψ∧φ∧χ↔∀xψ∧∀xφ∧∀xχ
18 17 biimpri ⊢∀xψ∧∀xφ∧∀xχ→∀xψ∧φ∧χ
19 16 18 e2 ⊢φ→∀xφ,ψ∧φ∧χ→∀xψ∧φ∧χ
20 19 in2 ⊢φ→∀xφ→ψ∧φ∧χ→∀xψ∧φ∧χ
21 20 in1 ⊢φ→∀xφ→ψ∧φ∧χ→∀xψ∧φ∧χ