Theorem alimdv 1918

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

Syntax hints:   → wi 4  ∀wal 1540

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

This theorem is referenced by:  2alimdv  1920  ax12v2  2187  ax13lem1  2379  axc16i  2441  mo4  2567  ralimdv2  3146  mo2icl  3673  sstr2OLD  3942  reuss2  4279  ssuni  4889  disjss2  5069  disjss1  5072  disjiun  5087  disjss3  5098  alxfr  5353  axprlem1  5369  axprlem2  5370  axpr  5373  axprOLD  5377  frss  5589  ssrel  5733  ssrel2  5735  ssrelrel  5746  fvn0ssdmfun  7021  dff3  7047  dfwe2  7721  trom  7819  findcard3  9187  dffi2  9330  indcardi  9955  zorn2lem4  10413  uzindi  13909  caubnd  15286  ramtlecl  16932  psgnunilem4  19430  nrhmzr  20474  dfconn2  23367  wilthlem3  27040  disjss1f  32650  ssrelf  32696  axsepg2  35240  axsepg2ALT  35241  ss2mcls  35764  mclsax  35765  wzel  36018  onsuct0  36637  bj-zfauscl  37127  wl-ax13lem1  37701  wl-eujustlem1  37795  axc11next  44714  traxext  45285  iscnrm3lem2  49247  setrec1lem2  50000