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

Theorem alimdv 1875
Description: Deduction form of Theorem 19.20 of [Margaris] p. 90, see alim 1773. (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 1869 . 2 (𝜑 → ∀𝑥𝜑)
2 alimdv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2alimdh 1780 1 (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1505
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1758  ax-4 1772  ax-5 1869
This theorem is referenced by:  2alimdv  1877  ax12v2  2108  sbequivvOLD  2255  ax13lem1  2303  axc16i  2372  ralimdv2  3120  mo2icl  3613  sstr2  3859  reuss2  4164  ssuni  4728  disjss2  4894  disjss1  4897  disjiun  4911  disjss3  4922  alxfr  5155  axprlem1  5174  axprlem2  5175  axpr  5179  frss  5368  ssrel  5501  ssrel2  5503  ssrelrel  5513  iotaval  6157  fvn0ssdmfun  6661  dff3  6683  dfwe2  7306  ordom  7399  findcard3  8550  dffi2  8676  indcardi  9255  zorn2lem4  9713  uzindi  13159  caubnd  14573  ramtlecl  16186  psgnunilem4  18381  dfconn2  21725  wilthlem3  25343  disjss1f  30083  ssrelf  30124  ss2mcls  32335  mclsax  32336  wzel  32632  onsuct0  33309  bj-zfauscl  33738  wl-ax13lem1  34187  axc11next  40155  nrhmzr  43508  setrec1lem2  44158
  Copyright terms: Public domain W3C validator