Theorem alimdv 1913

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

Syntax hints:   → wi 4  ∀wal 1531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1792  ax-4 1806  ax-5 1907

This theorem is referenced by:  2alimdv  1915  ax12v2  2175  sbequivvOLD  2330  ax13lem1  2388  axc16i  2454  mo4  2646  ralimdv2  3176  mo2icl  3704  sstr2  3973  reuss2  4282  ssuni  4862  disjss2  5033  disjss1  5036  disjiun  5052  disjss3  5064  alxfr  5307  axprlem1  5323  axprlem2  5324  axpr  5328  frss  5521  ssrel  5656  ssrel2  5658  ssrelrel  5668  iotaval  6328  fvn0ssdmfun  6841  dff3  6865  dfwe2  7495  ordom  7588  findcard3  8760  dffi2  8886  indcardi  9466  zorn2lem4  9920  uzindi  13349  caubnd  14717  ramtlecl  16335  psgnunilem4  18624  dfconn2  22026  wilthlem3  25646  disjss1f  30321  ssrelf  30365  ss2mcls  32815  mclsax  32816  wzel  33111  onsuct0  33789  bj-zfauscl  34243  wl-ax13lem1  34745  axc11next  40736  nrhmzr  44143  setrec1lem2  44790