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

Theorem ralimi2 2978
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 1779 . 2 (∀𝑥(𝑥𝐴𝜑) → ∀𝑥(𝑥𝐵𝜓))
3 df-ral 2946 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
4 df-ral 2946 . 2 (∀𝑥𝐵 𝜓 ↔ ∀𝑥(𝑥𝐵𝜓))
52, 3, 43imtr4i 281 1 (∀𝑥𝐴 𝜑 → ∀𝑥𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1521  wcel 2030  wral 2941
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777
This theorem depends on definitions:  df-bi 197  df-ral 2946
This theorem is referenced by:  ralimia  2979  ralcom3  3134  tfi  7095  resixpfo  7988  omex  8578  kmlem1  9010  brdom5  9389  brdom4  9390  xrub  12180  pcmptcl  15642  itgeq2  23589  iblcnlem  23600  pntrsumbnd  25300  nmounbseqi  27760  nmounbseqiALT  27761  sumdmdi  29407  dmdbr4ati  29408  dmdbr6ati  29410  bnj110  31054  fiinfi  38195
  Copyright terms: Public domain W3C validator