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

Theorem ralimdv2 2990
Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 1-Feb-2005.)
Hypothesis
Ref Expression
ralimdv2.1 (𝜑 → ((𝑥𝐴𝜓) → (𝑥𝐵𝜒)))
Assertion
Ref Expression
ralimdv2 (𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐵 𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)   𝐵(𝑥)

Proof of Theorem ralimdv2
StepHypRef Expression
1 ralimdv2.1 . . 3 (𝜑 → ((𝑥𝐴𝜓) → (𝑥𝐵𝜒)))
21alimdv 1885 . 2 (𝜑 → (∀𝑥(𝑥𝐴𝜓) → ∀𝑥(𝑥𝐵𝜒)))
3 df-ral 2946 . 2 (∀𝑥𝐴 𝜓 ↔ ∀𝑥(𝑥𝐴𝜓))
4 df-ral 2946 . 2 (∀𝑥𝐵 𝜒 ↔ ∀𝑥(𝑥𝐵𝜒))
52, 3, 43imtr4g 285 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  ax-5 1879
This theorem depends on definitions:  df-bi 197  df-ral 2946
This theorem is referenced by:  ralimdva  2991  ssralv  3699  zorn2lem7  9362  pwfseqlem3  9520  sup2  11017  xrsupexmnf  12173  xrinfmexpnf  12174  xrsupsslem  12175  xrinfmsslem  12176  xrub  12180  r19.29uz  14134  rexuzre  14136  caurcvg  14451  caucvg  14453  isprm5  15466  prmgaplem5  15806  prmgaplem6  15807  mrissmrid  16348  elcls3  20935  iscnp4  21115  cncls2  21125  cnntr  21127  2ndcsep  21310  dyadmbllem  23413  xrlimcnp  24740  pntlem3  25343  sigaclfu2  30312  mapdordlem2  37243  iunrelexp0  38311  climrec  40153  0ellimcdiv  40199
  Copyright terms: Public domain W3C validator