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

Theorem ral2imi 2931
 Description: Inference quantifying antecedent, nested antecedent, and consequent, with a strong hypothesis. (Contributed by NM, 19-Dec-2006.) Allow shortening of ralim 2932. (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 2901 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 ral2imi.1 . . . . 5 (𝜑 → (𝜓𝜒))
32imim3i 62 . . . 4 ((𝑥𝐴𝜑) → ((𝑥𝐴𝜓) → (𝑥𝐴𝜒)))
43al2imi 1733 . . 3 (∀𝑥(𝑥𝐴𝜑) → (∀𝑥(𝑥𝐴𝜓) → ∀𝑥(𝑥𝐴𝜒)))
5 df-ral 2901 . . 3 (∀𝑥𝐴 𝜓 ↔ ∀𝑥(𝑥𝐴𝜓))
6 df-ral 2901 . . 3 (∀𝑥𝐴 𝜒 ↔ ∀𝑥(𝑥𝐴𝜒))
74, 5, 63imtr4g 284 . 2 (∀𝑥(𝑥𝐴𝜑) → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜒))
81, 7sylbi 206 1 (∀𝑥𝐴 𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∀wal 1473   ∈ wcel 1977  ∀wral 2896 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728 This theorem depends on definitions:  df-bi 196  df-ral 2901 This theorem is referenced by:  ralim  2932  rexim  2991  r19.26  3046  iiner  7706  ss2ixp  7807  undifixp  7830  boxriin  7836  acni2  8752  axcc4  9144  intgru  9515  ingru  9516  prdsdsval3  15968  mrcmndind  17189  hauscmplem  21019  usg2wlkeq  26236  prdstotbnd  32763  uspgr2wlkeq  40854  1wlkp1lem8  40889
 Copyright terms: Public domain W3C validator