Theorem alimdv 1946

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1825  ax-4 1839  ax-5 1940

This theorem is used by:  2alimdv  1948  ax12v2  2215  ax13lem1  2406  axc16i  2468  mo4  2594  ralimdv2  3174  mo2icl  3677  reuss2  4279  ssuni  4898  disjss2  5079  disjss1  5082  disjiun  5097  disjss3  5108  alxfr  5378  axprlem2  5395  axpr  5398  axprlem1OLD  5399  axprOLD  5403  axprglem  5407  frss  5625  ssrel  5769  ssrel2  5771  ssrelrel  5782  fvn0ssdmfun  7069  dff3  7095  dfwe2  7769  trom  7867  findcard3  9239  dffi2  9379  indcardi  10030  zorn2lem4  10487  uzindi  14023  caubnd  15415  ramtlecl  17064  psgnunilem4  19571  nrhmzr  20645  dfconn2  23585  wilthlem3  27243  disjss1f  32926  ssrelf  32969  axprALT2  35512  axsepg3  35562  axsepg3ALT  35563  axpowg2  35568  axpowg3  35569  ss2mcls  36068  mclsax  36069  wzel  36322  onsuct0  36980  axtco2  37013  mh-regprimbi  37084  bj-sepg  37587  bj-axseprep  37739  wl-ax13lem1  38168  wl-eujustlem1  38271  axc11next  45144  traxext  45714  iscnrm3lem2  49741  setrec1lem2  50494