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

Theorem ralimdv2 3145
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 1898 . 2 (𝜑 → (∀𝑥(𝑥𝐴𝜓) → ∀𝑥(𝑥𝐵𝜒)))
3 df-ral 3112 . 2 (∀𝑥𝐴 𝜓 ↔ ∀𝑥(𝑥𝐴𝜓))
4 df-ral 3112 . 2 (∀𝑥𝐵 𝜒 ↔ ∀𝑥(𝑥𝐵𝜒))
52, 3, 43imtr4g 297 1 (𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1523  wcel 2083  wral 3107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892
This theorem depends on definitions:  df-bi 208  df-ral 3112
This theorem is referenced by:  ralimdva  3146  ssralv  3960  zorn2lem7  9777  pwfseqlem3  9935  sup2  11451  xrsupexmnf  12552  xrinfmexpnf  12553  xrsupsslem  12554  xrinfmsslem  12555  xrub  12559  r19.29uz  14548  rexuzre  14550  caurcvg  14871  caucvg  14873  isprm5  15884  prmgaplem5  16224  prmgaplem6  16225  mrissmrid  16745  elcls3  21379  iscnp4  21559  cncls2  21569  cnntr  21571  2ndcsep  21755  dyadmbllem  23887  xrlimcnp  25232  pntlem3  25871  sigaclfu2  30993  lfuhgr2  31975  rdgssun  34211  mapdordlem2  38325  dffltz  38789  iunrelexp0  39553  climrec  41447  0ellimcdiv  41493
  Copyright terms: Public domain W3C validator