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  7073  dff3  7099  dfwe2  7779  trom  7877  findcard3  9250  dffi2  9390  indcardi  10041  zorn2lem4  10498  uzindi  14040  caubnd  15438  ramtlecl  17086  psgnunilem4  19615  nrhmzr  20690  dfconn2  23630  wilthlem3  27289  disjss1f  32992  ssrelf  33035  axprALT2  35565  axsepg3  35615  axsepg3ALT  35616  axpowg2  35621  axpowg3  35622  ss2mcls  36101  mclsax  36102  wzel  36355  onsuct0  37013  axtco2  37046  mh-regprimbi  37117  bj-sepg  37620  bj-axseprep  37772  wl-ax13lem1  38201  wl-eujustlem1  38304  findcard4  38426  axc11next  45193  traxext  45763  iscnrm3lem2  49789  setrec1lem2  50542