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

Theorem alrim3con13v 41612
 Description: Closed form of alrimi 2211 with 2 additional conjuncts having no occurrences of the quantifying variable. This proof is 19.21a3con13vVD 41931 automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
alrim3con13v ((𝜑 → ∀𝑥𝜑) → ((𝜓𝜑𝜒) → ∀𝑥(𝜓𝜑𝜒)))
Distinct variable groups:   𝜓,𝑥   𝜒,𝑥
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem alrim3con13v
StepHypRef Expression
1 simp1 1133 . . . . 5 ((𝜓𝜑𝜒) → 𝜓)
21a1i 11 . . . 4 ((𝜑 → ∀𝑥𝜑) → ((𝜓𝜑𝜒) → 𝜓))
3 ax-5 1911 . . . 4 (𝜓 → ∀𝑥𝜓)
42, 3syl6 35 . . 3 ((𝜑 → ∀𝑥𝜑) → ((𝜓𝜑𝜒) → ∀𝑥𝜓))
5 simp2 1134 . . . 4 ((𝜓𝜑𝜒) → 𝜑)
65imim1i 63 . . 3 ((𝜑 → ∀𝑥𝜑) → ((𝜓𝜑𝜒) → ∀𝑥𝜑))
7 simp3 1135 . . . . 5 ((𝜓𝜑𝜒) → 𝜒)
87a1i 11 . . . 4 ((𝜑 → ∀𝑥𝜑) → ((𝜓𝜑𝜒) → 𝜒))
9 ax-5 1911 . . . 4 (𝜒 → ∀𝑥𝜒)
108, 9syl6 35 . . 3 ((𝜑 → ∀𝑥𝜑) → ((𝜓𝜑𝜒) → ∀𝑥𝜒))
114, 6, 103jcad 1126 . 2 ((𝜑 → ∀𝑥𝜑) → ((𝜓𝜑𝜒) → (∀𝑥𝜓 ∧ ∀𝑥𝜑 ∧ ∀𝑥𝜒)))
12 19.26-3an 1873 . 2 (∀𝑥(𝜓𝜑𝜒) ↔ (∀𝑥𝜓 ∧ ∀𝑥𝜑 ∧ ∀𝑥𝜒))
1311, 12syl6ibr 255 1 ((𝜑 → ∀𝑥𝜑) → ((𝜓𝜑𝜒) → ∀𝑥(𝜓𝜑𝜒)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ w3a 1084  ∀wal 1536 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911 This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1086 This theorem is referenced by:  tratrbVD  41940
 Copyright terms: Public domain W3C validator