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

Theorem ralimdv2 2955
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 1842 . 2 (𝜑 → (∀𝑥(𝑥𝐴𝜓) → ∀𝑥(𝑥𝐵𝜒)))
3 df-ral 2912 . 2 (∀𝑥𝐴 𝜓 ↔ ∀𝑥(𝑥𝐴𝜓))
4 df-ral 2912 . 2 (∀𝑥𝐵 𝜒 ↔ ∀𝑥(𝑥𝐵𝜒))
52, 3, 43imtr4g 285 1 (𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1478  wcel 1987  wral 2907
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836
This theorem depends on definitions:  df-bi 197  df-ral 2912
This theorem is referenced by:  ralimdva  2956  ssralv  3645  zorn2lem7  9268  pwfseqlem3  9426  sup2  10923  xrsupexmnf  12078  xrinfmexpnf  12079  xrsupsslem  12080  xrinfmsslem  12081  xrub  12085  r19.29uz  14024  rexuzre  14026  caurcvg  14341  caucvg  14343  isprm5  15343  prmgaplem5  15683  prmgaplem6  15684  mrissmrid  16222  elcls3  20797  iscnp4  20977  cncls2  20987  cnntr  20989  2ndcsep  21172  dyadmbllem  23273  xrlimcnp  24595  pntlem3  25198  sigaclfu2  29962  mapdordlem2  36403  iunrelexp0  37472  climrec  39236  0ellimcdiv  39282
  Copyright terms: Public domain W3C validator