Theorem alimdv 1917

Description: Deduction form of Theorem 19.20 of [Margaris] p. 90, see alim 1812. See alimdh 1819 and alimd 2210 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

Step	Hyp	Ref	Expression
1		ax-5 1911	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		alimdv.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	alimdh 1819	1 ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))

Syntax hints:   → wi 4  ∀wal 1536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1797  ax-4 1811  ax-5 1911

This theorem is referenced by:  2alimdv  1919  ax12v2  2177  ax13lem1  2381  axc16i  2447  mo4  2584  ralimdv2  3107  mo2icl  3630  sstr2  3901  reuss2  4219  ssuni  4828  disjss2  5004  disjss1  5007  disjiun  5023  disjss3  5035  alxfr  5280  axprlem1  5296  axprlem2  5297  axpr  5301  frss  5495  ssrel  5631  ssrel2  5633  ssrelrel  5643  iotaval  6314  fvn0ssdmfun  6839  dff3  6863  dfwe2  7501  ordom  7594  findcard3  8807  dffi2  8933  indcardi  9514  zorn2lem4  9972  uzindi  13412  caubnd  14779  ramtlecl  16404  psgnunilem4  18705  dfconn2  22132  wilthlem3  25767  disjss1f  30446  ssrelf  30490  ss2mcls  33058  mclsax  33059  wzel  33385  onsuct0  34213  bj-zfauscl  34682  wl-ax13lem1  35225  axc11next  41518  nrhmzr  44913  iscnrm3lem2  45667  setrec1lem2  45703