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 39235
Description: Closed form of alrimi 2249 with 2 additional conjuncts having no occurrences of the quantifying variable. This proof is 19.21a3con13vVD 39575 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 1159 . . . . 5 ((𝜓𝜑𝜒) → 𝜓)
21a1i 11 . . . 4 ((𝜑 → ∀𝑥𝜑) → ((𝜓𝜑𝜒) → 𝜓))
3 ax-5 2001 . . . 4 (𝜓 → ∀𝑥𝜓)
42, 3syl6 35 . . 3 ((𝜑 → ∀𝑥𝜑) → ((𝜓𝜑𝜒) → ∀𝑥𝜓))
5 simp2 1160 . . . 4 ((𝜓𝜑𝜒) → 𝜑)
65imim1i 63 . . 3 ((𝜑 → ∀𝑥𝜑) → ((𝜓𝜑𝜒) → ∀𝑥𝜑))
7 simp3 1161 . . . . 5 ((𝜓𝜑𝜒) → 𝜒)
87a1i 11 . . . 4 ((𝜑 → ∀𝑥𝜑) → ((𝜓𝜑𝜒) → 𝜒))
9 ax-5 2001 . . . 4 (𝜒 → ∀𝑥𝜒)
108, 9syl6 35 . . 3 ((𝜑 → ∀𝑥𝜑) → ((𝜓𝜑𝜒) → ∀𝑥𝜒))
114, 6, 103jcad 1152 . 2 ((𝜑 → ∀𝑥𝜑) → ((𝜓𝜑𝜒) → (∀𝑥𝜓 ∧ ∀𝑥𝜑 ∧ ∀𝑥𝜒)))
12 19.26-3an 1961 . 2 (∀𝑥(𝜓𝜑𝜒) ↔ (∀𝑥𝜓 ∧ ∀𝑥𝜑 ∧ ∀𝑥𝜒))
1311, 12syl6ibr 243 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
This theorem is referenced by:  tratrbVD  39585
  Copyright terms: Public domain W3C validator