Theorem alimdv 1938

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

Syntax hints:   → wi 4  ∀wal 1560

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

This theorem is referenced by:  2alimdv  1940  ax12v2  2216  ax13lem1  2407  axc16i  2469  mo4  2595  ralimdv2  3173  mo2icl  3679  reuss2  4280  ssuni  4893  disjss2  5072  disjss1  5075  disjiun  5090  disjss3  5101  alxfr  5366  axprlem2  5383  axpr  5386  axprlem1OLD  5387  axprOLD  5391  axprglem  5395  frss  5613  ssrel  5757  ssrel2  5759  ssrelrel  5770  fvn0ssdmfun  7057  dff3  7083  dfwe2  7759  trom  7857  findcard3  9229  dffi2  9371  indcardi  9999  zorn2lem4  10458  uzindi  13997  caubnd  15388  ramtlecl  17038  psgnunilem4  19539  nrhmzr  20589  dfconn2  23481  wilthlem3  27136  disjss1f  32774  ssrelf  32819  axprALT2  35409  axsepg3  35441  axsepg3ALT  35442  axpowg2  35447  axpowg3  35448  ss2mcls  35923  mclsax  35924  wzel  36177  onsuct0  36806  axtco2  36839  mh-regprimbi  36910  bj-zfauscl  37414  bj-axseprep  37564  wl-ax13lem1  37993  wl-eujustlem1  38096  axc11next  44987  traxext  45558  iscnrm3lem2  49561  setrec1lem2  50314