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

Theorem ral2imi 3085
Description: Inference quantifying antecedent, nested antecedent, and consequent, with a strong hypothesis. (Contributed by NM, 19-Dec-2006.) Allow shortening of ralim 3086. (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 3062 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 ral2imi.1 . . . . 5 (𝜑 → (𝜓𝜒))
32imim3i 64 . . . 4 ((𝑥𝐴𝜑) → ((𝑥𝐴𝜓) → (𝑥𝐴𝜒)))
43al2imi 1815 . . 3 (∀𝑥(𝑥𝐴𝜑) → (∀𝑥(𝑥𝐴𝜓) → ∀𝑥(𝑥𝐴𝜒)))
5 df-ral 3062 . . 3 (∀𝑥𝐴 𝜓 ↔ ∀𝑥(𝑥𝐴𝜓))
6 df-ral 3062 . . 3 (∀𝑥𝐴 𝜒 ↔ ∀𝑥(𝑥𝐴𝜒))
74, 5, 63imtr4g 296 . 2 (∀𝑥(𝑥𝐴𝜑) → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜒))
81, 7sylbi 217 1 (∀𝑥𝐴 𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1538  wcel 2108  wral 3061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809
This theorem depends on definitions:  df-bi 207  df-ral 3062
This theorem is referenced by:  ralim  3086  rexim  3087  ralbi  3103  r19.26  3111  iiner  8829  ss2ixp  8950  undifixp  8974  boxriin  8980  acni2  10086  axcc4  10479  intgru  10854  ingru  10855  prdsdsval3  17530  mndind  18841  hauscmplem  23414  uspgr2wlkeq  29664  wlkp1lem8  29698  prdstotbnd  37801  mnuunid  44296
  Copyright terms: Public domain W3C validator