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

Theorem ralimdv2 3162
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 1915 . 2 (𝜑 → (∀𝑥(𝑥𝐴𝜓) → ∀𝑥(𝑥𝐵𝜒)))
3 df-ral 3061 . 2 (∀𝑥𝐴 𝜓 ↔ ∀𝑥(𝑥𝐴𝜓))
4 df-ral 3061 . 2 (∀𝑥𝐵 𝜒 ↔ ∀𝑥(𝑥𝐵𝜒))
52, 3, 43imtr4g 296 1 (𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1537  wcel 2107  wral 3060
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909
This theorem depends on definitions:  df-bi 207  df-ral 3061
This theorem is referenced by:  ralimdva  3166  ssralvOLD  4055  zorn2lem7  10543  pwfseqlem3  10701  sup2  12225  xrsupexmnf  13348  xrinfmexpnf  13349  xrsupsslem  13350  xrinfmsslem  13351  xrub  13355  r19.29uz  15390  rexuzre  15392  caurcvg  15714  caucvg  15716  isprm5  16745  prmgaplem5  17094  prmgaplem6  17095  mrissmrid  17685  elcls3  23092  iscnp4  23272  cncls2  23282  cnntr  23284  2ndcsep  23468  dyadmbllem  25635  xrlimcnp  27012  pntlem3  27654  fldextrspunlsplem  33724  sigaclfu2  34123  lfuhgr2  35125  rdgssun  37380  mapdordlem2  41640  aks6d1c1  42118  sn-sup2  42506  dffltz  42649  cantnfresb  43342  safesnsupfiub  43434  iunrelexp0  43720  climrec  45623  0ellimcdiv  45669  pgindnf  49290
  Copyright terms: Public domain W3C validator