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

Theorem ralimi2 3154
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 1803 . 2 (∀𝑥(𝑥𝐴𝜑) → ∀𝑥(𝑥𝐵𝜓))
3 df-ral 3140 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
4 df-ral 3140 . 2 (∀𝑥𝐵 𝜓 ↔ ∀𝑥(𝑥𝐵𝜓))
52, 3, 43imtr4i 293 1 (∀𝑥𝐴 𝜑 → ∀𝑥𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1526  wcel 2105  wral 3135
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801
This theorem depends on definitions:  df-bi 208  df-ral 3140
This theorem is referenced by:  ralimia  3155  ralcom3  3362  tfi  7557  resixpfo  8488  omex  9094  kmlem1  9564  brdom5  9939  brdom4  9940  xrub  12693  pcmptcl  16215  itgeq2  24305  iblcnlem  24316  pntrsumbnd  26069  nmounbseqi  28481  nmounbseqiALT  28482  sumdmdi  30124  dmdbr4ati  30125  dmdbr6ati  30127  bnj110  32029  fiinfi  39810
  Copyright terms: Public domain W3C validator