Theorem alimdv 1924

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

Syntax hints:   → wi 4  ∀wal 1546

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1803  ax-4 1817  ax-5 1918

This theorem is referenced by:  2alimdv  1926  ax12v2  2193  ax13lem1  2384  axc16i  2446  mo4  2572  ralimdv2  3150  mo2icl  3657  reuss2  4257  ssuni  4866  disjss2  5045  disjss1  5048  disjiun  5063  disjss3  5074  alxfr  5339  axprlem2  5356  axpr  5359  axprlem1OLD  5360  axprOLD  5364  axprglem  5368  frss  5585  ssrel  5729  ssrel2  5731  ssrelrel  5742  fvn0ssdmfun  7019  dff3  7045  dfwe2  7721  trom  7819  findcard3  9187  dffi2  9330  indcardi  9958  zorn2lem4  10416  uzindi  13939  caubnd  15316  ramtlecl  16966  psgnunilem4  19467  nrhmzr  20513  dfconn2  23406  wilthlem3  27055  disjss1f  32665  ssrelf  32711  axprALT2  35305  axsepg3  35337  axsepg3ALT  35338  axpowg2  35343  axpowg3  35344  ss2mcls  35811  mclsax  35812  wzel  36065  onsuct0  36684  axtco2  36717  mh-regprimbi  36788  bj-zfauscl  37292  bj-axseprep  37442  wl-ax13lem1  37871  wl-eujustlem1  37974  axc11next  44865  traxext  45436  iscnrm3lem2  49439  setrec1lem2  50192