Theorem alimdv 1917

Description: Deduction form of Theorem 19.20 of [Margaris] p. 90, see alim 1811. See alimdh 1818 and alimd 2215 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  2182  ax13lem1  2374  axc16i  2436  mo4  2561  ralimdv2  3141  mo2icl  3668  sstr2OLD  3937  reuss2  4273  ssuni  4881  disjss2  5059  disjss1  5062  disjiun  5077  disjss3  5088  alxfr  5343  axprlem1  5359  axprlem2  5360  axpr  5363  axprOLD  5367  frss  5578  ssrel  5722  ssrel2  5724  ssrelrel  5735  fvn0ssdmfun  7007  dff3  7033  dfwe2  7707  trom  7805  findcard3  9167  dffi2  9307  indcardi  9932  zorn2lem4  10390  uzindi  13889  caubnd  15266  ramtlecl  16912  psgnunilem4  19409  nrhmzr  20452  dfconn2  23334  wilthlem3  27007  disjss1f  32552  ssrelf  32598  axsepg2  35094  axsepg2ALT  35095  ss2mcls  35612  mclsax  35613  wzel  35866  onsuct0  36485  bj-zfauscl  36968  wl-ax13lem1  37538  axc11next  44498  traxext  45069  iscnrm3lem2  49034  setrec1lem2  49788