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 ( ( 𝜑 → ∀ 𝑥 𝜑 ) → ( ( 𝜓 ∧ 𝜑 ∧ 𝜒 ) → ∀ 𝑥 ( 𝜓 ∧ 𝜑 ∧ 𝜒 ) ) )

Proof

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