Theorem alimdv 1919

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

Syntax hints:   → wi 4  ∀wal 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1798  ax-4 1812  ax-5 1913

This theorem is referenced by:  2alimdv  1921  ax12v2  2173  ax13lem1  2374  axc16i  2436  mo4  2566  ralimdv2  3107  mo2icl  3649  sstr2  3928  reuss2  4249  ssuni  4866  disjss2  5042  disjss1  5045  disjiun  5061  disjss3  5073  alxfr  5330  axprlem1  5346  axprlem2  5347  axpr  5351  frss  5556  ssrel  5693  ssrelOLD  5694  ssrel2  5696  ssrelrel  5706  iotaval  6407  fvn0ssdmfun  6952  dff3  6976  dfwe2  7624  trom  7721  findcard3  9057  dffi2  9182  indcardi  9797  zorn2lem4  10255  uzindi  13702  caubnd  15070  ramtlecl  16701  psgnunilem4  19105  dfconn2  22570  wilthlem3  26219  disjss1f  30911  ssrelf  30955  ss2mcls  33530  mclsax  33531  wzel  33818  onsuct0  34630  bj-zfauscl  35112  wl-ax13lem1  35665  axc11next  42024  nrhmzr  45431  iscnrm3lem2  46228  setrec1lem2  46394