Theorem alimdv 1949

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1828  ax-4 1842  ax-5 1943

This theorem is used by:  2alimdv  1951  ax12v2  2218  ax13lem1  2408  axc16i  2470  mo4  2596  ralimdv2  3176  mo2icl  3679  reuss2  4279  ssuni  4900  disjss2  5081  disjss1  5084  disjiun  5099  disjss3  5110  alxfr  5380  axprlem2  5397  axpr  5400  axprlem1OLD  5401  axprOLD  5405  axprglem  5409  frss  5627  ssrel  5771  ssrel2  5773  ssrelrel  5784  fvn0ssdmfun  7074  dff3  7100  dfwe2  7780  trom  7878  findcard3  9251  dffi2  9391  indcardi  10042  zorn2lem4  10499  uzindi  14041  caubnd  15439  ramtlecl  17087  psgnunilem4  19616  nrhmzr  20691  dfconn2  23631  wilthlem3  27290  disjss1f  32993  ssrelf  33036  axprALT2  35566  axsepg3  35616  axsepg3ALT  35617  axpowg2  35622  axpowg3  35623  ss2mcls  36102  mclsax  36103  wzel  36356  onsuct0  37014  axtco2  37047  mh-regprimbi  37118  bj-sepg  37621  bj-axseprep  37773  wl-ax13lem1  38202  wl-eujustlem1  38305  findcard4  38427  axc11next  45194  traxext  45764  iscnrm3lem2  49790  setrec1lem2  50543