Theorem alimdv 1916

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

Syntax hints:   → wi 4  ∀wal 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem is referenced by:  2alimdv  1918  ax12v2  2180  ax13lem1  2372  axc16i  2434  mo4  2559  ralimdv2  3142  mo2icl  3685  sstr2OLD  3954  reuss2  4289  ssuni  4896  disjss2  5077  disjss1  5080  disjiun  5095  disjss3  5106  alxfr  5362  axprlem1  5378  axprlem2  5379  axpr  5382  axprOLD  5386  frss  5602  ssrel  5745  ssrelOLD  5746  ssrel2  5748  ssrelrel  5759  iotavalOLD  6485  fvn0ssdmfun  7046  dff3  7072  dfwe2  7750  trom  7851  findcard3  9229  findcard3OLD  9230  dffi2  9374  indcardi  9994  zorn2lem4  10452  uzindi  13947  caubnd  15325  ramtlecl  16971  psgnunilem4  19427  nrhmzr  20446  dfconn2  23306  wilthlem3  26980  disjss1f  32501  ssrelf  32543  axsepg2  35072  axsepg2ALT  35073  ss2mcls  35555  mclsax  35556  wzel  35812  onsuct0  36429  bj-zfauscl  36912  wl-ax13lem1  37482  axc11next  44395  traxext  44967  iscnrm3lem2  48920  setrec1lem2  49674