Theorem alimdv 1949

Description: Deduction form of Theorem 19.20 of [Margaris] p. 90, see alim 1843. See alimdh 1850 and alimd 2249 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 1943	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		alimdv.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	alimdh 1850	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 1828  ax-4 1842  ax-5 1943

This theorem is used by:  2alimdv  1951  ax12v2  2215  ax13lem1  2404  axc16i  2466  mo4  2592  ralimdv2  3172  mo2icl  3672  reuss2  4272  ssuni  4893  disjss2  5073  disjss1  5076  disjiun  5091  disjss3  5102  alxfr  5369  axprlem2  5386  axpr  5389  axprlem1OLD  5390  axprglem  5394  frss  5615  ssrel  5759  ssrel2  5761  ssrelrel  5772  fvn0ssdmfun  7074  dff3  7100  dfwe2  7788  trom  7886  findcard3  9274  dffi2  9415  setrec1lem2  9967  indcardi  10120  zorn2lem4  10577  uzindi  14125  caubnd  15526  ramtlecl  17178  psgnunilem4  19711  nrhmzr  20789  dfconn2  23737  wilthlem3  27397  disjss1f  33166  ssrelf  33209  axprALT2  35734  axsepg3  35809  axsepg3ALT  35810  axpowg2  35815  axpowg3  35816  ss2mcls  36333  mclsax  36334  wzel  36586  onsuct0  37229  axtco2  37262  mh-regprimbi  37333  bj-sepg  37836  bj-axseprep  37990  wl-ax13lem1  38417  wl-eujustlem1  38520  findcard4  38632  axc11next  45389  traxext  45966  iscnrm3lem2  50042