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

Theorem alimdv 1908
Description: Deduction form of Theorem 19.20 of [Margaris] p. 90, see alim 1802. See alimdh 1809 and alimd 2203 for versions without a distinct variable condition. (Contributed by NM, 3-Apr-1994.)
Hypothesis
Ref Expression
alimdv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
alimdv (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem alimdv
StepHypRef Expression
1 ax-5 1902 . 2 (𝜑 → ∀𝑥𝜑)
2 alimdv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2alimdh 1809 1 (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1526
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1787  ax-4 1801  ax-5 1902
This theorem is referenced by:  2alimdv  1910  ax12v2  2169  sbequivvOLD  2326  ax13lem1  2385  axc16i  2453  mo4  2646  ralimdv2  3176  mo2icl  3704  sstr2  3973  reuss2  4282  ssuni  4854  disjss2  5026  disjss1  5029  disjiun  5045  disjss3  5057  alxfr  5299  axprlem1  5315  axprlem2  5316  axpr  5320  frss  5516  ssrel  5651  ssrel2  5653  ssrelrel  5663  iotaval  6323  fvn0ssdmfun  6835  dff3  6859  dfwe2  7484  ordom  7577  findcard3  8750  dffi2  8876  indcardi  9456  zorn2lem4  9910  uzindi  13340  caubnd  14708  ramtlecl  16326  psgnunilem4  18556  dfconn2  21957  wilthlem3  25575  disjss1f  30251  ssrelf  30295  ss2mcls  32713  mclsax  32714  wzel  33009  onsuct0  33687  bj-zfauscl  34141  wl-ax13lem1  34629  axc11next  40618  nrhmzr  44042  setrec1lem2  44689
  Copyright terms: Public domain W3C validator