Theorem alimdv 1919

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

Syntax hints:   → wi 4  ∀wal 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1797  ax-4 1811  ax-5 1913

This theorem is referenced by:  2alimdv  1921  ax12v2  2173  ax13lem1  2373  axc16i  2435  mo4  2560  ralimdv2  3163  mo2icl  3710  sstr2  3989  reuss2  4315  ssuni  4936  disjss2  5116  disjss1  5119  disjiun  5135  disjss3  5147  alxfr  5405  axprlem1  5421  axprlem2  5422  axpr  5426  frss  5643  ssrel  5782  ssrelOLD  5783  ssrel2  5785  ssrelrel  5796  iotavalOLD  6517  fvn0ssdmfun  7076  dff3  7101  dfwe2  7760  trom  7863  findcard3  9284  findcard3OLD  9285  dffi2  9417  indcardi  10035  zorn2lem4  10493  uzindi  13946  caubnd  15304  ramtlecl  16932  psgnunilem4  19364  dfconn2  22922  wilthlem3  26571  disjss1f  31798  ssrelf  31839  ss2mcls  34554  mclsax  34555  wzel  34791  onsuct0  35321  bj-zfauscl  35799  wl-ax13lem1  36370  axc11next  43155  nrhmzr  46637  iscnrm3lem2  47557  setrec1lem2  47723