Theorem alimdv 1920

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

Syntax hints:   → wi 4  ∀wal 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem is referenced by:  2alimdv  1922  ax12v2  2174  ax13lem1  2374  axc16i  2436  mo4  2561  ralimdv2  3164  mo2icl  3711  sstr2  3990  reuss2  4316  ssuni  4937  disjss2  5117  disjss1  5120  disjiun  5136  disjss3  5148  alxfr  5406  axprlem1  5422  axprlem2  5423  axpr  5427  frss  5644  ssrel  5783  ssrelOLD  5784  ssrel2  5786  ssrelrel  5797  iotavalOLD  6518  fvn0ssdmfun  7077  dff3  7102  dfwe2  7761  trom  7864  findcard3  9285  findcard3OLD  9286  dffi2  9418  indcardi  10036  zorn2lem4  10494  uzindi  13947  caubnd  15305  ramtlecl  16933  psgnunilem4  19365  dfconn2  22923  wilthlem3  26574  disjss1f  31834  ssrelf  31875  ss2mcls  34590  mclsax  34591  wzel  34827  onsuct0  35374  bj-zfauscl  35852  wl-ax13lem1  36423  axc11next  43213  nrhmzr  46695  iscnrm3lem2  47615  setrec1lem2  47781