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  3682  sstr2OLD  3951  reuss2  4285  ssuni  4892  disjss2  5072  disjss1  5075  disjiun  5090  disjss3  5101  alxfr  5357  axprlem1  5373  axprlem2  5374  axpr  5377  axprOLD  5381  frss  5595  ssrel  5737  ssrel2  5739  ssrelrel  5750  iotavalOLD  6473  fvn0ssdmfun  7028  dff3  7054  dfwe2  7730  trom  7831  findcard3  9205  findcard3OLD  9206  dffi2  9350  indcardi  9970  zorn2lem4  10428  uzindi  13923  caubnd  15301  ramtlecl  16947  psgnunilem4  19411  nrhmzr  20457  dfconn2  23339  wilthlem3  27013  disjss1f  32551  ssrelf  32593  axsepg2  35065  axsepg2ALT  35066  ss2mcls  35548  mclsax  35549  wzel  35805  onsuct0  36422  bj-zfauscl  36905  wl-ax13lem1  37475  axc11next  44388  traxext  44960  iscnrm3lem2  48916  setrec1lem2  49670