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

Theorem alimdv 1997
Description: Deduction form of Theorem 19.20 of [Margaris] p. 90, see alim 1886. (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 1991 . 2 (𝜑 → ∀𝑥𝜑)
2 alimdv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2alimdh 1893 1 (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1629
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1870  ax-4 1885  ax-5 1991
This theorem is referenced by:  2alimdv  1999  ax12v2  2205  ax13lem1  2410  axc16i  2472  ralimdv2  3110  mo2icl  3537  sstr2  3759  reuss2  4055  ssuni  4596  disjss2  4757  disjss1  4760  disjiun  4774  disjss3  4785  alxfr  5007  frss  5216  ssrel  5345  ssrelOLD  5346  ssrel2  5348  ssrelrel  5358  iotaval  6003  fvn0ssdmfun  6492  dff3  6514  dfwe2  7128  ordom  7221  findcard3  8359  dffi2  8485  indcardi  9064  zorn2lem4  9523  uzindi  12985  caubnd  14302  ramtlecl  15907  psgnunilem4  18120  dfconn2  21439  wilthlem3  25013  disjss1f  29720  ssrelf  29761  ss2mcls  31799  mclsax  31800  wzel  32102  onsuct0  32773  bj-ssbim  32955  bj-zfauscl  33249  wl-ax13lem1  33622  wl-ax8clv2  33710  axc11next  39130  nrhmzr  42398  setrec1lem2  42960
  Copyright terms: Public domain W3C validator