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

Theorem ralimi2 3077
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 1810 . 2 (∀𝑥(𝑥𝐴𝜑) → ∀𝑥(𝑥𝐵𝜓))
3 df-ral 3061 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
4 df-ral 3061 . 2 (∀𝑥𝐵 𝜓 ↔ ∀𝑥(𝑥𝐵𝜓))
52, 3, 43imtr4i 292 1 (∀𝑥𝐴 𝜑 → ∀𝑥𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1537  wcel 2107  wral 3060
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808
This theorem depends on definitions:  df-bi 207  df-ral 3061
This theorem is referenced by:  ralimia  3079  ralcom3OLD  3097  tfi  7875  resixpfo  8977  omex  9684  kmlem1  10192  brdom5  10570  brdom4  10571  xrub  13355  pcmptcl  16930  itgeq2  25814  iblcnlem  25825  pntrsumbnd  27611  nmounbseqi  30797  nmounbseqiALT  30798  sumdmdi  32440  dmdbr4ati  32441  dmdbr6ati  32443  bnj110  34873  fiinfi  43591
  Copyright terms: Public domain W3C validator