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

Theorem ralimi2 3080
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 1819 . 2 (∀𝑥(𝑥𝐴𝜑) → ∀𝑥(𝑥𝐵𝜓))
3 df-ral 3066 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
4 df-ral 3066 . 2 (∀𝑥𝐵 𝜓 ↔ ∀𝑥(𝑥𝐵𝜓))
52, 3, 43imtr4i 295 1 (∀𝑥𝐴 𝜑 → ∀𝑥𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1541  wcel 2110  wral 3061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817
This theorem depends on definitions:  df-bi 210  df-ral 3066
This theorem is referenced by:  ralimia  3081  ralcom3  3276  tfi  7632  resixpfo  8617  omex  9258  kmlem1  9764  brdom5  10143  brdom4  10144  xrub  12902  pcmptcl  16444  itgeq2  24675  iblcnlem  24686  pntrsumbnd  26447  nmounbseqi  28858  nmounbseqiALT  28859  sumdmdi  30501  dmdbr4ati  30502  dmdbr6ati  30504  bnj110  32551  fiinfi  40856
  Copyright terms: Public domain W3C validator