MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ral2imi Structured version   Visualization version   GIF version

Theorem ral2imi 3086
Description: Inference quantifying antecedent, nested antecedent, and consequent, with a strong hypothesis. (Contributed by NM, 19-Dec-2006.) Allow shortening of ralim 3087. (Revised by Wolf Lammen, 1-Dec-2019.)
Hypothesis
Ref Expression
ral2imi.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
ral2imi (∀𝑥𝐴 𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜒))

Proof of Theorem ral2imi
StepHypRef Expression
1 df-ral 3063 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 ral2imi.1 . . . . 5 (𝜑 → (𝜓𝜒))
32imim3i 64 . . . 4 ((𝑥𝐴𝜑) → ((𝑥𝐴𝜓) → (𝑥𝐴𝜒)))
43al2imi 1817 . . 3 (∀𝑥(𝑥𝐴𝜑) → (∀𝑥(𝑥𝐴𝜓) → ∀𝑥(𝑥𝐴𝜒)))
5 df-ral 3063 . . 3 (∀𝑥𝐴 𝜓 ↔ ∀𝑥(𝑥𝐴𝜓))
6 df-ral 3063 . . 3 (∀𝑥𝐴 𝜒 ↔ ∀𝑥(𝑥𝐴𝜒))
74, 5, 63imtr4g 295 . 2 (∀𝑥(𝑥𝐴𝜑) → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜒))
81, 7sylbi 216 1 (∀𝑥𝐴 𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1539  wcel 2106  wral 3062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811
This theorem depends on definitions:  df-bi 206  df-ral 3063
This theorem is referenced by:  ralim  3087  rexim  3088  ralbi  3104  r19.26  3112  iiner  8686  ss2ixp  8806  undifixp  8830  boxriin  8836  acni2  9940  axcc4  10333  intgru  10708  ingru  10709  prdsdsval3  17327  mndind  18598  hauscmplem  22709  uspgr2wlkeq  28423  wlkp1lem8  28457  prdstotbnd  36191  mnuunid  42468
  Copyright terms: Public domain W3C validator