Theorem alimdv 1943

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

Syntax hints:   → wi 4  ∀wal 1565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem is referenced by:  2alimdv  1945  ax12v2  2221  ax13lem1  2412  axc16i  2474  mo4  2600  ralimdv2  3180  mo2icl  3686  reuss2  4287  ssuni  4902  disjss2  5083  disjss1  5086  disjiun  5101  disjss3  5112  alxfr  5379  axprlem2  5396  axpr  5399  axprlem1OLD  5400  axprOLD  5404  axprglem  5408  frss  5626  ssrel  5770  ssrel2  5772  ssrelrel  5783  fvn0ssdmfun  7070  dff3  7096  dfwe2  7773  trom  7871  findcard3  9243  dffi2  9383  indcardi  10025  zorn2lem4  10483  uzindi  14018  caubnd  15410  ramtlecl  17060  psgnunilem4  19567  nrhmzr  20622  dfconn2  23545  wilthlem3  27200  disjss1f  32858  ssrelf  32901  axprALT2  35446  axsepg3  35487  axsepg3ALT  35488  axpowg2  35493  axpowg3  35494  ss2mcls  35993  mclsax  35994  wzel  36247  onsuct0  36875  axtco2  36908  mh-regprimbi  36979  bj-zfauscl  37482  bj-axseprep  37633  wl-ax13lem1  38062  wl-eujustlem1  38165  axc11next  45042  traxext  45612  iscnrm3lem2  49632  setrec1lem2  50385