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

Theorem ralimdv2 3146
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 1917 . 2 (𝜑 → (∀𝑥(𝑥𝐴𝜓) → ∀𝑥(𝑥𝐵𝜒)))
3 df-ral 3114 . 2 (∀𝑥𝐴 𝜓 ↔ ∀𝑥(𝑥𝐴𝜓))
4 df-ral 3114 . 2 (∀𝑥𝐵 𝜒 ↔ ∀𝑥(𝑥𝐵𝜒))
52, 3, 43imtr4g 299 1 (𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1536  wcel 2112  wral 3109
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911
This theorem depends on definitions:  df-bi 210  df-ral 3114
This theorem is referenced by:  ralimdva  3147  ssralv  3984  zorn2lem7  9917  pwfseqlem3  10075  sup2  11588  xrsupexmnf  12690  xrinfmexpnf  12691  xrsupsslem  12692  xrinfmsslem  12693  xrub  12697  r19.29uz  14706  rexuzre  14708  caurcvg  15029  caucvg  15031  isprm5  16045  prmgaplem5  16385  prmgaplem6  16386  mrissmrid  16908  elcls3  21692  iscnp4  21872  cncls2  21882  cnntr  21884  2ndcsep  22068  dyadmbllem  24207  xrlimcnp  25558  pntlem3  26197  sigaclfu2  31494  lfuhgr2  32479  rdgssun  34796  mapdordlem2  38932  sn-sup2  39591  dffltz  39612  iunrelexp0  40400  climrec  42242  0ellimcdiv  42288
  Copyright terms: Public domain W3C validator