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

Theorem ralimdv2 3149
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 2007 . 2 (𝜑 → (∀𝑥(𝑥𝐴𝜓) → ∀𝑥(𝑥𝐵𝜒)))
3 df-ral 3101 . 2 (∀𝑥𝐴 𝜓 ↔ ∀𝑥(𝑥𝐴𝜓))
4 df-ral 3101 . 2 (∀𝑥𝐵 𝜒 ↔ ∀𝑥(𝑥𝐵𝜒))
52, 3, 43imtr4g 287 1 (𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1635  wcel 2156  wral 3096
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001
This theorem depends on definitions:  df-bi 198  df-ral 3101
This theorem is referenced by:  ralimdva  3150  ssralv  3863  zorn2lem7  9609  pwfseqlem3  9767  sup2  11264  xrsupexmnf  12353  xrinfmexpnf  12354  xrsupsslem  12355  xrinfmsslem  12356  xrub  12360  r19.29uz  14313  rexuzre  14315  caurcvg  14630  caucvg  14632  isprm5  15636  prmgaplem5  15976  prmgaplem6  15977  mrissmrid  16506  elcls3  21101  iscnp4  21281  cncls2  21291  cnntr  21293  2ndcsep  21476  dyadmbllem  23580  xrlimcnp  24909  pntlem3  25512  sigaclfu2  30509  mapdordlem2  37418  iunrelexp0  38494  climrec  40315  0ellimcdiv  40361
  Copyright terms: Public domain W3C validator