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

Theorem alimdv 2007
Description: Deduction form of Theorem 19.20 of [Margaris] p. 90, see alim 1895. (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 2001 . 2 (𝜑 → ∀𝑥𝜑)
2 alimdv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2alimdh 1902 1 (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1635
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1877  ax-4 1894  ax-5 2001
This theorem is referenced by:  2alimdv  2009  ax12v2  2216  ax13lem1  2422  axc16i  2484  ralimdv2  3149  mo2icl  3583  sstr2  3805  reuss2  4108  ssuni  4654  disjss2  4815  disjss1  4818  disjiun  4832  disjss3  4843  alxfr  5076  frss  5278  ssrel  5409  ssrelOLD  5410  ssrel2  5412  ssrelrel  5422  iotaval  6075  fvn0ssdmfun  6572  dff3  6594  dfwe2  7211  ordom  7304  findcard3  8442  dffi2  8568  indcardi  9147  zorn2lem4  9606  uzindi  13005  caubnd  14321  ramtlecl  15921  psgnunilem4  18118  dfconn2  21436  wilthlem3  25010  disjss1f  29711  ssrelf  29752  ss2mcls  31788  mclsax  31789  wzel  32090  onsuct0  32757  bj-ssbim  32937  bj-zfauscl  33232  wl-ax13lem1  33605  wl-ax8clv2  33694  axc11next  39106  nrhmzr  42441  setrec1lem2  43003
  Copyright terms: Public domain W3C validator