Theorem alimdv 1914

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

Syntax hints:   → wi 4  ∀wal 1535

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

This theorem is referenced by:  2alimdv  1916  ax12v2  2177  ax13lem1  2377  axc16i  2439  mo4  2564  ralimdv2  3161  mo2icl  3723  sstr2OLD  4003  reuss2  4332  ssuni  4937  disjss2  5118  disjss1  5121  disjiun  5136  disjss3  5147  alxfr  5413  axprlem1  5429  axprlem2  5430  axpr  5433  axprOLD  5437  frss  5653  ssrel  5795  ssrelOLD  5796  ssrel2  5798  ssrelrel  5809  iotavalOLD  6537  fvn0ssdmfun  7094  dff3  7120  dfwe2  7793  trom  7896  findcard3  9316  findcard3OLD  9317  dffi2  9461  indcardi  10079  zorn2lem4  10537  uzindi  14020  caubnd  15394  ramtlecl  17034  psgnunilem4  19530  nrhmzr  20554  dfconn2  23443  wilthlem3  27128  disjss1f  32592  ssrelf  32635  axsepg2  35075  axsepg2ALT  35076  ss2mcls  35553  mclsax  35554  wzel  35806  onsuct0  36424  bj-zfauscl  36907  wl-ax13lem1  37477  axc11next  44402  traxext  44938  iscnrm3lem2  48731  setrec1lem2  48919