Theorem alimdv 1920

Description: Deduction form of Theorem 19.20 of [Margaris] p. 90, see alim 1814. See alimdh 1821 and alimd 2208 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 1914	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		alimdv.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	alimdh 1821	1 ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))

Syntax hints:   → wi 4  ∀wal 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem is referenced by:  2alimdv  1922  ax12v2  2175  ax13lem1  2374  axc16i  2436  mo4  2566  ralimdv2  3101  mo2icl  3644  sstr2  3924  reuss2  4246  ssuni  4863  disjss2  5038  disjss1  5041  disjiun  5057  disjss3  5069  alxfr  5325  axprlem1  5341  axprlem2  5342  axpr  5346  frss  5547  ssrel  5683  ssrel2  5685  ssrelrel  5695  iotaval  6392  fvn0ssdmfun  6934  dff3  6958  dfwe2  7602  trom  7696  findcard3  8987  dffi2  9112  indcardi  9728  zorn2lem4  10186  uzindi  13630  caubnd  14998  ramtlecl  16629  psgnunilem4  19020  dfconn2  22478  wilthlem3  26124  disjss1f  30812  ssrelf  30856  ss2mcls  33430  mclsax  33431  wzel  33745  onsuct0  34557  bj-zfauscl  35039  wl-ax13lem1  35592  axc11next  41913  nrhmzr  45319  iscnrm3lem2  46116  setrec1lem2  46280