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

Theorem alimdv 1885
Description: Deduction form of Theorem 19.20 of [Margaris] p. 90, see alim 1778. (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 1879 . 2 (𝜑 → ∀𝑥𝜑)
2 alimdv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2alimdh 1785 1 (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1521
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1762  ax-4 1777  ax-5 1879
This theorem is referenced by:  2alimdv  1887  ax12v2  2089  ax13lem1  2284  axc16i  2353  ralimdv2  2990  mo2icl  3418  sstr2  3643  reuss2  3940  ssuni  4491  ssuniOLD  4492  disjss2  4655  disjss1  4658  disjiun  4672  disjss3  4684  alxfr  4908  frss  5110  ssrel  5241  ssrelOLD  5242  ssrel2  5244  ssrelrel  5254  iotaval  5900  fvn0ssdmfun  6390  dff3  6412  dfwe2  7023  ordom  7116  findcard3  8244  dffi2  8370  indcardi  8902  zorn2lem4  9359  uzindi  12821  caubnd  14142  ramtlecl  15751  psgnunilem4  17963  dfconn2  21270  wilthlem3  24841  disjss1f  29512  ssrelf  29553  ss2mcls  31591  mclsax  31592  wzel  31894  onsuct0  32565  bj-ssbim  32746  wl-ax13lem1  33417  wl-ax8clv2  33511  axc11next  38924  nrhmzr  42198  setrec1lem2  42760
  Copyright terms: Public domain W3C validator