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

Theorem ral2imi 3089
 Description: Inference quantifying antecedent, nested antecedent, and consequent, with a strong hypothesis. (Contributed by NM, 19-Dec-2006.) Allow shortening of ralim 3095. (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 3076 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 ral2imi.1 . . . . 5 (𝜑 → (𝜓𝜒))
32imim3i 64 . . . 4 ((𝑥𝐴𝜑) → ((𝑥𝐴𝜓) → (𝑥𝐴𝜒)))
43al2imi 1818 . . 3 (∀𝑥(𝑥𝐴𝜑) → (∀𝑥(𝑥𝐴𝜓) → ∀𝑥(𝑥𝐴𝜒)))
5 df-ral 3076 . . 3 (∀𝑥𝐴 𝜓 ↔ ∀𝑥(𝑥𝐴𝜓))
6 df-ral 3076 . . 3 (∀𝑥𝐴 𝜒 ↔ ∀𝑥(𝑥𝐴𝜒))
74, 5, 63imtr4g 300 . 2 (∀𝑥(𝑥𝐴𝜑) → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜒))
81, 7sylbi 220 1 (∀𝑥𝐴 𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∀wal 1537   ∈ wcel 2112  ∀wral 3071 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812 This theorem depends on definitions:  df-bi 210  df-ral 3076 This theorem is referenced by:  ralim  3095  ralbi  3100  r19.26  3102  rexim  3169  iiner  8380  ss2ixp  8493  undifixp  8517  boxriin  8523  acni2  9499  axcc4  9892  intgru  10267  ingru  10268  prdsdsval3  16809  mndind  18051  hauscmplem  22099  uspgr2wlkeq  27527  wlkp1lem8  27562  prdstotbnd  35505  mnuunid  41351
 Copyright terms: Public domain W3C validator