Theorem alimdv 1917

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

Syntax hints:   → wi 4  ∀wal 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem is referenced by:  2alimdv  1919  ax12v2  2184  ax13lem1  2376  axc16i  2438  mo4  2564  ralimdv2  3143  mo2icl  3670  sstr2OLD  3939  reuss2  4276  ssuni  4886  disjss2  5066  disjss1  5069  disjiun  5084  disjss3  5095  alxfr  5350  axprlem1  5366  axprlem2  5367  axpr  5370  axprOLD  5374  frss  5586  ssrel  5730  ssrel2  5732  ssrelrel  5743  fvn0ssdmfun  7017  dff3  7043  dfwe2  7717  trom  7815  findcard3  9181  dffi2  9324  indcardi  9949  zorn2lem4  10407  uzindi  13903  caubnd  15280  ramtlecl  16926  psgnunilem4  19424  nrhmzr  20468  dfconn2  23361  wilthlem3  27034  disjss1f  32596  ssrelf  32642  axsepg2  35187  axsepg2ALT  35188  ss2mcls  35711  mclsax  35712  wzel  35965  onsuct0  36584  bj-zfauscl  37068  wl-ax13lem1  37638  wl-eujustlem1  37732  axc11next  44589  traxext  45160  iscnrm3lem2  49122  setrec1lem2  49875