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

Theorem alimdv 1920
Description: Deduction form of Theorem 19.20 of [Margaris] p. 90, see alim 1813. See alimdh 1820 and alimd 2206 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 1914 . 2 (𝜑 → ∀𝑥𝜑)
2 alimdv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2alimdh 1820 1 (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1798  ax-4 1812  ax-5 1914
This theorem is referenced by:  2alimdv  1922  ax12v2  2174  ax13lem1  2373  axc16i  2435  mo4  2561  ralimdv2  3157  mo2icl  3676  sstr2  3955  reuss2  4279  ssuni  4897  disjss2  5077  disjss1  5080  disjiun  5096  disjss3  5108  alxfr  5366  axprlem1  5382  axprlem2  5383  axpr  5387  frss  5604  ssrel  5742  ssrelOLD  5743  ssrel2  5745  ssrelrel  5756  iotavalOLD  6474  fvn0ssdmfun  7029  dff3  7054  dfwe2  7712  trom  7815  findcard3  9235  findcard3OLD  9236  dffi2  9367  indcardi  9985  zorn2lem4  10443  uzindi  13896  caubnd  15252  ramtlecl  16880  psgnunilem4  19287  dfconn2  22793  wilthlem3  26442  disjss1f  31543  ssrelf  31587  ss2mcls  34226  mclsax  34227  wzel  34462  onsuct0  34966  bj-zfauscl  35444  wl-ax13lem1  36015  axc11next  42778  nrhmzr  46261  iscnrm3lem2  47057  setrec1lem2  47223
  Copyright terms: Public domain W3C validator