Theorem alimdv 1917

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

Syntax hints:   → wi 4  ∀wal 1535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem is referenced by:  2alimdv  1919  ax12v2  2179  sbequivvOLD  2334  ax13lem1  2392  axc16i  2458  mo4  2650  ralimdv2  3178  mo2icl  3707  sstr2  3976  reuss2  4285  ssuni  4865  disjss2  5036  disjss1  5039  disjiun  5055  disjss3  5067  alxfr  5310  axprlem1  5326  axprlem2  5327  axpr  5331  frss  5524  ssrel  5659  ssrel2  5661  ssrelrel  5671  iotaval  6331  fvn0ssdmfun  6844  dff3  6868  dfwe2  7498  ordom  7591  findcard3  8763  dffi2  8889  indcardi  9469  zorn2lem4  9923  uzindi  13353  caubnd  14720  ramtlecl  16338  psgnunilem4  18627  dfconn2  22029  wilthlem3  25649  disjss1f  30324  ssrelf  30368  ss2mcls  32817  mclsax  32818  wzel  33113  onsuct0  33791  bj-zfauscl  34245  wl-ax13lem1  34748  axc11next  40745  nrhmzr  44151  setrec1lem2  44798