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

Theorem ralimdv2 3173
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 1908 . 2 (𝜑 → (∀𝑥(𝑥𝐴𝜓) → ∀𝑥(𝑥𝐵𝜒)))
3 df-ral 3140 . 2 (∀𝑥𝐴 𝜓 ↔ ∀𝑥(𝑥𝐴𝜓))
4 df-ral 3140 . 2 (∀𝑥𝐵 𝜒 ↔ ∀𝑥(𝑥𝐵𝜒))
52, 3, 43imtr4g 297 1 (𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1526  wcel 2105  wral 3135
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902
This theorem depends on definitions:  df-bi 208  df-ral 3140
This theorem is referenced by:  ralimdva  3174  ssralv  4030  zorn2lem7  9912  pwfseqlem3  10070  sup2  11585  xrsupexmnf  12686  xrinfmexpnf  12687  xrsupsslem  12688  xrinfmsslem  12689  xrub  12693  r19.29uz  14698  rexuzre  14700  caurcvg  15021  caucvg  15023  isprm5  16039  prmgaplem5  16379  prmgaplem6  16380  mrissmrid  16900  elcls3  21619  iscnp4  21799  cncls2  21809  cnntr  21811  2ndcsep  21995  dyadmbllem  24127  xrlimcnp  25473  pntlem3  26112  sigaclfu2  31279  lfuhgr2  32262  rdgssun  34541  mapdordlem2  38653  dffltz  39149  iunrelexp0  39925  climrec  41760  0ellimcdiv  41806
  Copyright terms: Public domain W3C validator