Theorem alimdv 1875

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

Syntax hints:   → wi 4  ∀wal 1505

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1758  ax-4 1772  ax-5 1869

This theorem is referenced by:  2alimdv  1877  ax12v2  2108  sbequivvOLD  2255  ax13lem1  2303  axc16i  2372  ralimdv2  3120  mo2icl  3613  sstr2  3859  reuss2  4164  ssuni  4728  disjss2  4894  disjss1  4897  disjiun  4911  disjss3  4922  alxfr  5155  axprlem1  5174  axprlem2  5175  axpr  5179  frss  5368  ssrel  5501  ssrel2  5503  ssrelrel  5513  iotaval  6157  fvn0ssdmfun  6661  dff3  6683  dfwe2  7306  ordom  7399  findcard3  8550  dffi2  8676  indcardi  9255  zorn2lem4  9713  uzindi  13159  caubnd  14573  ramtlecl  16186  psgnunilem4  18381  dfconn2  21725  wilthlem3  25343  disjss1f  30083  ssrelf  30124  ss2mcls  32335  mclsax  32336  wzel  32632  onsuct0  33309  bj-zfauscl  33738  wl-ax13lem1  34187  axc11next  40155  nrhmzr  43508  setrec1lem2  44158