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  2378  axc16i  2440  mo4  2566  ralimdv2  3146  mo2icl  3660  sstr2OLD  3929  reuss2  4266  ssuni  4875  disjss2  5055  disjss1  5058  disjiun  5073  disjss3  5084  alxfr  5349  axprlem2  5366  axpr  5369  axprlem1OLD  5370  axprOLD  5374  axprglem  5378  frss  5595  ssrel  5739  ssrel2  5741  ssrelrel  5752  fvn0ssdmfun  7026  dff3  7052  dfwe2  7728  trom  7826  findcard3  9193  dffi2  9336  indcardi  9963  zorn2lem4  10421  uzindi  13944  caubnd  15321  ramtlecl  16971  psgnunilem4  19472  nrhmzr  20514  dfconn2  23384  wilthlem3  27033  disjss1f  32642  ssrelf  32688  axsepg2  35225  axsepg2ALT  35226  axprALT2  35253  ss2mcls  35750  mclsax  35751  wzel  36004  onsuct0  36623  axtco2  36656  mh-regprimbi  36727  bj-zfauscl  37231  bj-axseprep  37381  wl-ax13lem1  37810  wl-eujustlem1  37913  axc11next  44833  traxext  45404  iscnrm3lem2  49410  setrec1lem2  50163