Theorem alimdv 1950

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1827  ax-4 1841  ax-5 1944

This theorem is used by:  2alimdv  1952  ax12v2  2217  ax13lem1  2406  axc16i  2468  mo4  2594  ralimdv2  3175  mo2icl  3675  reuss2  4274  ssuni  4896  disjss2  5076  disjss1  5079  disjiun  5094  disjss3  5105  alxfr  5373  axprlem2  5390  axpr  5393  axprlem1OLD  5394  axprglem  5398  frss  5619  ssrel  5764  ssrel2  5766  ssrelrel  5777  fvn0ssdmfun  7085  dff3  7111  dfwe2  7798  trom  7896  findcard3  9288  dffi2  9428  setrec1lem2  9980  indcardi  10133  zorn2lem4  10590  uzindi  14138  caubnd  15541  ramtlecl  17193  psgnunilem4  19726  nrhmzr  20804  dfconn2  23752  wilthlem3  27412  disjss1f  33223  ssrelf  33266  axprALT2  35798  dfac16  35828  axsepg3  35883  axsepg3ALT  35884  axpowg2  35889  axpowg3  35890  onprcf1of1orbd  36011  ss2mcls  36457  mclsax  36458  elpssmo  36591  wzel  36719  onsuct0  37362  axtco2  37395  mh-regprimbi  37466  bj-sepg  37969  bj-axseprep  38135  wl-ax13lem1  38563  wl-eujustlem1  38666  findcard4  38778  axc11next  45536  traxext  46112  iscnrm3lem2  50194