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

Theorem alrim3con13v 39268
Description: Closed form of alrimi 2238 with 2 additional conjuncts having no occurrences of the quantifying variable. This proof is 19.21a3con13vVD 39609 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 1130 . . . . 5 ((𝜓𝜑𝜒) → 𝜓)
21a1i 11 . . . 4 ((𝜑 → ∀𝑥𝜑) → ((𝜓𝜑𝜒) → 𝜓))
3 ax-5 1991 . . . 4 (𝜓 → ∀𝑥𝜓)
42, 3syl6 35 . . 3 ((𝜑 → ∀𝑥𝜑) → ((𝜓𝜑𝜒) → ∀𝑥𝜓))
5 simp2 1131 . . . 4 ((𝜓𝜑𝜒) → 𝜑)
65imim1i 63 . . 3 ((𝜑 → ∀𝑥𝜑) → ((𝜓𝜑𝜒) → ∀𝑥𝜑))
7 simp3 1132 . . . . 5 ((𝜓𝜑𝜒) → 𝜒)
87a1i 11 . . . 4 ((𝜑 → ∀𝑥𝜑) → ((𝜓𝜑𝜒) → 𝜒))
9 ax-5 1991 . . . 4 (𝜒 → ∀𝑥𝜒)
108, 9syl6 35 . . 3 ((𝜑 → ∀𝑥𝜑) → ((𝜓𝜑𝜒) → ∀𝑥𝜒))
114, 6, 103jcad 1123 . 2 ((𝜑 → ∀𝑥𝜑) → ((𝜓𝜑𝜒) → (∀𝑥𝜓 ∧ ∀𝑥𝜑 ∧ ∀𝑥𝜒)))
12 19.26-3an 1951 . 2 (∀𝑥(𝜓𝜑𝜒) ↔ (∀𝑥𝜓 ∧ ∀𝑥𝜑 ∧ ∀𝑥𝜒))
1311, 12syl6ibr 242 1 ((𝜑 → ∀𝑥𝜑) → ((𝜓𝜑𝜒) → ∀𝑥(𝜓𝜑𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1071  wal 1629
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991
This theorem depends on definitions:  df-bi 197  df-an 383  df-3an 1073
This theorem is referenced by:  tratrbVD  39619
  Copyright terms: Public domain W3C validator