Theorem alimdv 1915

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

Syntax hints:   → wi 4  ∀wal 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1794  ax-4 1808  ax-5 1909

This theorem is referenced by:  2alimdv  1917  ax12v2  2178  ax13lem1  2378  axc16i  2440  mo4  2565  ralimdv2  3162  mo2icl  3719  sstr2OLD  3990  reuss2  4325  ssuni  4931  disjss2  5112  disjss1  5115  disjiun  5130  disjss3  5141  alxfr  5406  axprlem1  5422  axprlem2  5423  axpr  5426  axprOLD  5430  frss  5648  ssrel  5791  ssrelOLD  5792  ssrel2  5794  ssrelrel  5805  iotavalOLD  6534  fvn0ssdmfun  7093  dff3  7119  dfwe2  7795  trom  7897  findcard3  9319  findcard3OLD  9320  dffi2  9464  indcardi  10082  zorn2lem4  10540  uzindi  14024  caubnd  15398  ramtlecl  17039  psgnunilem4  19516  nrhmzr  20538  dfconn2  23428  wilthlem3  27114  disjss1f  32586  ssrelf  32628  axsepg2  35097  axsepg2ALT  35098  ss2mcls  35574  mclsax  35575  wzel  35826  onsuct0  36443  bj-zfauscl  36926  wl-ax13lem1  37496  axc11next  44430  traxext  44999  iscnrm3lem2  48839  setrec1lem2  49262