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 39401
Description: Virtual deduction proof of alrim3con13v 39060. 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 39173 (   (𝜑 → ∀𝑥𝜑)   ,   (𝜓 𝜑𝜒)   ▶   𝜓   )
4:2,?: e2 39173 (   (𝜑 → ∀𝑥𝜑)   ,   (𝜓 𝜑𝜒)   ▶   𝜑   )
5:2,?: e2 39173 (   (𝜑 → ∀𝑥𝜑)   ,   (𝜓 𝜑𝜒)   ▶   𝜒   )
6:1,4,?: e12 39268 (   (𝜑 → ∀𝑥𝜑)   ,   (𝜓 𝜑𝜒)   ▶   𝑥𝜑   )
7:3,?: e2 39173 (   (𝜑 → ∀𝑥𝜑)   ,   (𝜓 𝜑𝜒)   ▶   𝑥𝜓   )
8:5,?: e2 39173 (   (𝜑 → ∀𝑥𝜑)   ,   (𝜓 𝜑𝜒)   ▶   𝑥𝜒   )
9:7,6,8,?: e222 39178 (   (𝜑 → ∀𝑥𝜑)   ,   (𝜓 𝜑𝜒)   ▶   (∀𝑥𝜓 ∧ ∀𝑥𝜑 ∧ ∀𝑥𝜒)   )
10:9,?: e2 39173 (   (𝜑 → ∀𝑥𝜑)   ,   (𝜓 𝜑𝜒)   ▶   𝑥(𝜓𝜑𝜒)   )
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 39155 . . . . . . 7 (   (𝜑 → ∀𝑥𝜑)   ,   (𝜓𝜑𝜒)   ▶   (𝜓𝜑𝜒)   )
2 simp1 1081 . . . . . . 7 ((𝜓𝜑𝜒) → 𝜓)
31, 2e2 39173 . . . . . 6 (   (𝜑 → ∀𝑥𝜑)   ,   (𝜓𝜑𝜒)   ▶   𝜓   )
4 ax-5 1879 . . . . . 6 (𝜓 → ∀𝑥𝜓)
53, 4e2 39173 . . . . 5 (   (𝜑 → ∀𝑥𝜑)   ,   (𝜓𝜑𝜒)   ▶   𝑥𝜓   )
6 idn1 39107 . . . . . 6 (   (𝜑 → ∀𝑥𝜑)   ▶   (𝜑 → ∀𝑥𝜑)   )
7 simp2 1082 . . . . . . 7 ((𝜓𝜑𝜒) → 𝜑)
81, 7e2 39173 . . . . . 6 (   (𝜑 → ∀𝑥𝜑)   ,   (𝜓𝜑𝜒)   ▶   𝜑   )
9 id 22 . . . . . 6 ((𝜑 → ∀𝑥𝜑) → (𝜑 → ∀𝑥𝜑))
106, 8, 9e12 39268 . . . . 5 (   (𝜑 → ∀𝑥𝜑)   ,   (𝜓𝜑𝜒)   ▶   𝑥𝜑   )
11 simp3 1083 . . . . . . 7 ((𝜓𝜑𝜒) → 𝜒)
121, 11e2 39173 . . . . . 6 (   (𝜑 → ∀𝑥𝜑)   ,   (𝜓𝜑𝜒)   ▶   𝜒   )
13 ax-5 1879 . . . . . 6 (𝜒 → ∀𝑥𝜒)
1412, 13e2 39173 . . . . 5 (   (𝜑 → ∀𝑥𝜑)   ,   (𝜓𝜑𝜒)   ▶   𝑥𝜒   )
15 pm3.2an3 1260 . . . . 5 (∀𝑥𝜓 → (∀𝑥𝜑 → (∀𝑥𝜒 → (∀𝑥𝜓 ∧ ∀𝑥𝜑 ∧ ∀𝑥𝜒))))
165, 10, 14, 15e222 39178 . . . 4 (   (𝜑 → ∀𝑥𝜑)   ,   (𝜓𝜑𝜒)   ▶   (∀𝑥𝜓 ∧ ∀𝑥𝜑 ∧ ∀𝑥𝜒)   )
17 19.26-3an 1840 . . . . 5 (∀𝑥(𝜓𝜑𝜒) ↔ (∀𝑥𝜓 ∧ ∀𝑥𝜑 ∧ ∀𝑥𝜒))
1817biimpri 218 . . . 4 ((∀𝑥𝜓 ∧ ∀𝑥𝜑 ∧ ∀𝑥𝜒) → ∀𝑥(𝜓𝜑𝜒))
1916, 18e2 39173 . . 3 (   (𝜑 → ∀𝑥𝜑)   ,   (𝜓𝜑𝜒)   ▶   𝑥(𝜓𝜑𝜒)   )
2019in2 39147 . 2 (   (𝜑 → ∀𝑥𝜑)   ▶   ((𝜓𝜑𝜒) → ∀𝑥(𝜓𝜑𝜒))   )
2120in1 39104 1 ((𝜑 → ∀𝑥𝜑) → ((𝜓𝜑𝜒) → ∀𝑥(𝜓𝜑𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1054  wal 1521
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879
This theorem depends on definitions:  df-bi 197  df-an 385  df-3an 1056  df-vd1 39103  df-vd2 39111
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator