Theorem alimdv 1918

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

Syntax hints:   → wi 4  ∀wal 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem is referenced by:  2alimdv  1920  ax12v2  2187  ax13lem1  2379  axc16i  2441  mo4  2567  ralimdv2  3147  mo2icl  3661  sstr2OLD  3930  reuss2  4267  ssuni  4876  disjss2  5056  disjss1  5059  disjiun  5074  disjss3  5085  alxfr  5346  axprlem2  5363  axpr  5366  axprlem1OLD  5367  axprOLD  5371  axprglem  5375  frss  5590  ssrel  5734  ssrel2  5736  ssrelrel  5747  fvn0ssdmfun  7022  dff3  7048  dfwe2  7723  trom  7821  findcard3  9188  dffi2  9331  indcardi  9958  zorn2lem4  10416  uzindi  13939  caubnd  15316  ramtlecl  16966  psgnunilem4  19467  nrhmzr  20509  dfconn2  23398  wilthlem3  27051  disjss1f  32661  ssrelf  32707  axsepg2  35245  axsepg2ALT  35246  axprALT2  35273  ss2mcls  35770  mclsax  35771  wzel  36024  onsuct0  36643  axtco2  36676  mh-regprimbi  36747  bj-zfauscl  37251  bj-axseprep  37401  wl-ax13lem1  37828  wl-eujustlem1  37931  axc11next  44855  traxext  45426  iscnrm3lem2  49426  setrec1lem2  50179