Theorem alimdv 1949

Description: Deduction form of Theorem 19.20 of [Margaris] p. 90, see alim 1843. See alimdh 1850 and alimd 2248 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  2215  ax13lem1  2403  axc16i  2465  mo4  2591  ralimdv2  3171  mo2icl  3672  reuss2  4272  ssuni  4893  disjss2  5073  disjss1  5076  disjiun  5091  disjss3  5102  alxfr  5372  axprlem2  5389  axpr  5392  axprlem1OLD  5393  axprOLD  5397  axprglem  5401  frss  5619  ssrel  5763  ssrel2  5765  ssrelrel  5776  fvn0ssdmfun  7069  dff3  7095  dfwe2  7775  trom  7873  findcard3  9257  dffi2  9397  indcardi  10066  zorn2lem4  10523  uzindi  14068  caubnd  15468  ramtlecl  17114  psgnunilem4  19647  nrhmzr  20725  dfconn2  23673  wilthlem3  27335  disjss1f  33074  ssrelf  33117  axprALT2  35647  axsepg3  35697  axsepg3ALT  35698  axpowg2  35703  axpowg3  35704  ss2mcls  36177  mclsax  36178  wzel  36431  onsuct0  37074  axtco2  37107  mh-regprimbi  37178  bj-sepg  37681  bj-axseprep  37833  wl-ax13lem1  38262  wl-eujustlem1  38365  findcard4  38477  axc11next  45244  traxext  45814  iscnrm3lem2  49875  setrec1lem2  50628