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

Theorem ralimi2 3067
Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 22-Feb-2004.)
Hypothesis
Ref Expression
ralimi2.1 ((𝑥𝐴𝜑) → (𝑥𝐵𝜓))
Assertion
Ref Expression
ralimi2 (∀𝑥𝐴 𝜑 → ∀𝑥𝐵 𝜓)

Proof of Theorem ralimi2
StepHypRef Expression
1 ralimi2.1 . . 3 ((𝑥𝐴𝜑) → (𝑥𝐵𝜓))
21alimi 1805 . 2 (∀𝑥(𝑥𝐴𝜑) → ∀𝑥(𝑥𝐵𝜓))
3 df-ral 3051 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
4 df-ral 3051 . 2 (∀𝑥𝐵 𝜓 ↔ ∀𝑥(𝑥𝐵𝜓))
52, 3, 43imtr4i 291 1 (∀𝑥𝐴 𝜑 → ∀𝑥𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1531  wcel 2098  wral 3050
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803
This theorem depends on definitions:  df-bi 206  df-ral 3051
This theorem is referenced by:  ralimia  3069  ralcom3OLD  3087  tfi  7862  resixpfo  8964  omex  9682  kmlem1  10189  brdom5  10568  brdom4  10569  xrub  13340  pcmptcl  16888  itgeq2  25790  iblcnlem  25801  pntrsumbnd  27587  nmounbseqi  30702  nmounbseqiALT  30703  sumdmdi  32345  dmdbr4ati  32346  dmdbr6ati  32348  bnj110  34671  fiinfi  43189
  Copyright terms: Public domain W3C validator