Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  19.21a3con13vVD Structured version   Visualization version   GIF version

Theorem 19.21a3con13vVD 39578
Description: Virtual deduction proof of alrim3con13v 39238. 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:: (   (𝜑 → ∀𝑥𝜑)    ▶   (𝜑 → ∀𝑥𝜑)   )
2:: (   (𝜑 → ∀𝑥𝜑)   ,   (𝜓𝜑 𝜒)   ▶   (𝜓𝜑𝜒)   )
3:2,?: e2 39351 (   (𝜑 → ∀𝑥𝜑)   ,   (𝜓 𝜑𝜒)   ▶   𝜓   )
4:2,?: e2 39351 (   (𝜑 → ∀𝑥𝜑)   ,   (𝜓 𝜑𝜒)   ▶   𝜑   )
5:2,?: e2 39351 (   (𝜑 → ∀𝑥𝜑)   ,   (𝜓 𝜑𝜒)   ▶   𝜒   )
6:1,4,?: e12 39445 (   (𝜑 → ∀𝑥𝜑)   ,   (𝜓 𝜑𝜒)   ▶   𝑥𝜑   )
7:3,?: e2 39351 (   (𝜑 → ∀𝑥𝜑)   ,   (𝜓 𝜑𝜒)   ▶   𝑥𝜓   )
8:5,?: e2 39351 (   (𝜑 → ∀𝑥𝜑)   ,   (𝜓 𝜑𝜒)   ▶   𝑥𝜒   )
9:7,6,8,?: e222 39356 (   (𝜑 → ∀𝑥𝜑)   ,   (𝜓 𝜑𝜒)   ▶   (∀𝑥𝜓 ∧ ∀𝑥𝜑 ∧ ∀𝑥𝜒)   )
10:9,?: e2 39351 (   (𝜑 → ∀𝑥𝜑)   ,   (𝜓 𝜑𝜒)   ▶   𝑥(𝜓𝜑𝜒)   )
11:10:in2 (   (𝜑 → ∀𝑥𝜑)   ▶   ((𝜓 𝜑𝜒) → ∀𝑥(𝜓𝜑𝜒))   )
qed:11:in1 ((𝜑 → ∀𝑥𝜑) → ((𝜓 𝜑𝜒) → ∀𝑥(𝜓𝜑𝜒)))
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
19.21a3con13vVD ((𝜑 → ∀𝑥𝜑) → ((𝜓𝜑𝜒) → ∀𝑥(𝜓𝜑𝜒)))
Distinct variable groups:   𝜓,𝑥   𝜒,𝑥
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem 19.21a3con13vVD
StepHypRef Expression
1 idn2 39333 . . . . . . 7 (   (𝜑 → ∀𝑥𝜑)   ,   (𝜓𝜑𝜒)   ▶   (𝜓𝜑𝜒)   )
2 simp1 1159 . . . . . . 7 ((𝜓𝜑𝜒) → 𝜓)
31, 2e2 39351 . . . . . 6 (   (𝜑 → ∀𝑥𝜑)   ,   (𝜓𝜑𝜒)   ▶   𝜓   )
4 ax-5 2001 . . . . . 6 (𝜓 → ∀𝑥𝜓)
53, 4e2 39351 . . . . 5 (   (𝜑 → ∀𝑥𝜑)   ,   (𝜓𝜑𝜒)   ▶   𝑥𝜓   )
6 idn1 39285 . . . . . 6 (   (𝜑 → ∀𝑥𝜑)   ▶   (𝜑 → ∀𝑥𝜑)   )
7 simp2 1160 . . . . . . 7 ((𝜓𝜑𝜒) → 𝜑)
81, 7e2 39351 . . . . . 6 (   (𝜑 → ∀𝑥𝜑)   ,   (𝜓𝜑𝜒)   ▶   𝜑   )
9 id 22 . . . . . 6 ((𝜑 → ∀𝑥𝜑) → (𝜑 → ∀𝑥𝜑))
106, 8, 9e12 39445 . . . . 5 (   (𝜑 → ∀𝑥𝜑)   ,   (𝜓𝜑𝜒)   ▶   𝑥𝜑   )
11 simp3 1161 . . . . . . 7 ((𝜓𝜑𝜒) → 𝜒)
121, 11e2 39351 . . . . . 6 (   (𝜑 → ∀𝑥𝜑)   ,   (𝜓𝜑𝜒)   ▶   𝜒   )
13 ax-5 2001 . . . . . 6 (𝜒 → ∀𝑥𝜒)
1412, 13e2 39351 . . . . 5 (   (𝜑 → ∀𝑥𝜑)   ,   (𝜓𝜑𝜒)   ▶   𝑥𝜒   )
15 pm3.2an3 1432 . . . . 5 (∀𝑥𝜓 → (∀𝑥𝜑 → (∀𝑥𝜒 → (∀𝑥𝜓 ∧ ∀𝑥𝜑 ∧ ∀𝑥𝜒))))
165, 10, 14, 15e222 39356 . . . 4 (   (𝜑 → ∀𝑥𝜑)   ,   (𝜓𝜑𝜒)   ▶   (∀𝑥𝜓 ∧ ∀𝑥𝜑 ∧ ∀𝑥𝜒)   )
17 19.26-3an 1961 . . . . 5 (∀𝑥(𝜓𝜑𝜒) ↔ (∀𝑥𝜓 ∧ ∀𝑥𝜑 ∧ ∀𝑥𝜒))
1817biimpri 219 . . . 4 ((∀𝑥𝜓 ∧ ∀𝑥𝜑 ∧ ∀𝑥𝜒) → ∀𝑥(𝜓𝜑𝜒))
1916, 18e2 39351 . . 3 (   (𝜑 → ∀𝑥𝜑)   ,   (𝜓𝜑𝜒)   ▶   𝑥(𝜓𝜑𝜒)   )
2019in2 39325 . 2 (   (𝜑 → ∀𝑥𝜑)   ▶   ((𝜓𝜑𝜒) → ∀𝑥(𝜓𝜑𝜒))   )
2120in1 39282 1 ((𝜑 → ∀𝑥𝜑) → ((𝜓𝜑𝜒) → ∀𝑥(𝜓𝜑𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1100  wal 1635
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001
This theorem depends on definitions:  df-bi 198  df-an 385  df-3an 1102  df-vd1 39281  df-vd2 39289
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator