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

Theorem ral2imi 3153
Description: Inference quantifying antecedent, nested antecedent, and consequent, with a strong hypothesis. (Contributed by NM, 19-Dec-2006.) Allow shortening of ralim 3159. (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 3140 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 ral2imi.1 . . . . 5 (𝜑 → (𝜓𝜒))
32imim3i 64 . . . 4 ((𝑥𝐴𝜑) → ((𝑥𝐴𝜓) → (𝑥𝐴𝜒)))
43al2imi 1807 . . 3 (∀𝑥(𝑥𝐴𝜑) → (∀𝑥(𝑥𝐴𝜓) → ∀𝑥(𝑥𝐴𝜒)))
5 df-ral 3140 . . 3 (∀𝑥𝐴 𝜓 ↔ ∀𝑥(𝑥𝐴𝜓))
6 df-ral 3140 . . 3 (∀𝑥𝐴 𝜒 ↔ ∀𝑥(𝑥𝐴𝜒))
74, 5, 63imtr4g 297 . 2 (∀𝑥(𝑥𝐴𝜑) → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜒))
81, 7sylbi 218 1 (∀𝑥𝐴 𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1526  wcel 2105  wral 3135
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801
This theorem depends on definitions:  df-bi 208  df-ral 3140
This theorem is referenced by:  ralim  3159  ralbi  3164  r19.26  3167  rexim  3238  iiner  8358  ss2ixp  8462  undifixp  8486  boxriin  8492  acni2  9460  axcc4  9849  intgru  10224  ingru  10225  prdsdsval3  16746  mndind  17980  hauscmplem  21942  uspgr2wlkeq  27354  wlkp1lem8  27389  prdstotbnd  34953  mnuunid  40490
  Copyright terms: Public domain W3C validator