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  3138  mo2icl  3674  sstr2OLD  3943  reuss2  4277  ssuni  4883  disjss2  5062  disjss1  5065  disjiun  5080  disjss3  5091  alxfr  5346  axprlem1  5362  axprlem2  5363  axpr  5366  axprOLD  5370  frss  5583  ssrel  5726  ssrel2  5728  ssrelrel  5739  fvn0ssdmfun  7008  dff3  7034  dfwe2  7710  trom  7808  findcard3  9172  dffi2  9313  indcardi  9935  zorn2lem4  10393  uzindi  13889  caubnd  15266  ramtlecl  16912  psgnunilem4  19376  nrhmzr  20422  dfconn2  23304  wilthlem3  26978  disjss1f  32516  ssrelf  32560  axsepg2  35055  axsepg2ALT  35056  ss2mcls  35551  mclsax  35552  wzel  35808  onsuct0  36425  bj-zfauscl  36908  wl-ax13lem1  37478  axc11next  44389  traxext  44961  iscnrm3lem2  48929  setrec1lem2  49683