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

Theorem ralimdv2 3091
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 1986 . 2 (𝜑 → (∀𝑥(𝑥𝐴𝜓) → ∀𝑥(𝑥𝐵𝜒)))
3 df-ral 3047 . 2 (∀𝑥𝐴 𝜓 ↔ ∀𝑥(𝑥𝐴𝜓))
4 df-ral 3047 . 2 (∀𝑥𝐵 𝜒 ↔ ∀𝑥(𝑥𝐵𝜒))
52, 3, 43imtr4g 285 1 (𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1622  wcel 2131  wral 3042
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980
This theorem depends on definitions:  df-bi 197  df-ral 3047
This theorem is referenced by:  ralimdva  3092  ssralv  3799  zorn2lem7  9508  pwfseqlem3  9666  sup2  11163  xrsupexmnf  12320  xrinfmexpnf  12321  xrsupsslem  12322  xrinfmsslem  12323  xrub  12327  r19.29uz  14281  rexuzre  14283  caurcvg  14598  caucvg  14600  isprm5  15613  prmgaplem5  15953  prmgaplem6  15954  mrissmrid  16495  elcls3  21081  iscnp4  21261  cncls2  21271  cnntr  21273  2ndcsep  21456  dyadmbllem  23559  xrlimcnp  24886  pntlem3  25489  sigaclfu2  30485  mapdordlem2  37420  iunrelexp0  38488  climrec  40330  0ellimcdiv  40376
  Copyright terms: Public domain W3C validator