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

Theorem ralimi2 3125
 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 1813 . 2 (∀𝑥(𝑥𝐴𝜑) → ∀𝑥(𝑥𝐵𝜓))
3 df-ral 3111 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
4 df-ral 3111 . 2 (∀𝑥𝐵 𝜓 ↔ ∀𝑥(𝑥𝐵𝜓))
52, 3, 43imtr4i 295 1 (∀𝑥𝐴 𝜑 → ∀𝑥𝐵 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∀wal 1536   ∈ wcel 2111  ∀wral 3106 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811 This theorem depends on definitions:  df-bi 210  df-ral 3111 This theorem is referenced by:  ralimia  3126  ralcom3  3318  tfi  7561  resixpfo  8501  omex  9108  kmlem1  9579  brdom5  9958  brdom4  9959  xrub  12713  pcmptcl  16237  itgeq2  24422  iblcnlem  24433  pntrsumbnd  26194  nmounbseqi  28604  nmounbseqiALT  28605  sumdmdi  30247  dmdbr4ati  30248  dmdbr6ati  30250  bnj110  32306  fiinfi  40443
 Copyright terms: Public domain W3C validator