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  3674  sstr2OLD  3943  reuss2  4280  ssuni  4890  disjss2  5070  disjss1  5073  disjiun  5088  disjss3  5099  alxfr  5356  axprlem1  5372  axprlem2  5373  axpr  5376  axprOLD  5380  axprglem  5384  frss  5598  ssrel  5742  ssrel2  5744  ssrelrel  5755  fvn0ssdmfun  7030  dff3  7056  dfwe2  7731  trom  7829  findcard3  9197  dffi2  9340  indcardi  9965  zorn2lem4  10423  uzindi  13919  caubnd  15296  ramtlecl  16942  psgnunilem4  19443  nrhmzr  20487  dfconn2  23380  wilthlem3  27053  disjss1f  32665  ssrelf  32711  axsepg2  35265  axsepg2ALT  35266  axprALT2  35293  ss2mcls  35790  mclsax  35791  wzel  36044  onsuct0  36663  bj-zfauscl  37199  bj-axseprep  37349  wl-ax13lem1  37776  wl-eujustlem1  37872  axc11next  44791  traxext  45362  iscnrm3lem2  49323  setrec1lem2  50076