Theorem alimdv 1915

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

Syntax hints:   → wi 4  ∀wal 1535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem is referenced by:  2alimdv  1917  ax12v2  2180  ax13lem1  2382  axc16i  2444  mo4  2569  ralimdv2  3169  mo2icl  3736  sstr2OLD  4016  reuss2  4345  ssuni  4956  disjss2  5136  disjss1  5139  disjiun  5154  disjss3  5165  alxfr  5425  axprlem1  5441  axprlem2  5442  axpr  5446  frss  5664  ssrel  5806  ssrelOLD  5807  ssrel2  5809  ssrelrel  5820  iotavalOLD  6547  fvn0ssdmfun  7108  dff3  7134  dfwe2  7809  trom  7912  findcard3  9346  findcard3OLD  9347  dffi2  9492  indcardi  10110  zorn2lem4  10568  uzindi  14033  caubnd  15407  ramtlecl  17047  psgnunilem4  19539  nrhmzr  20563  dfconn2  23448  wilthlem3  27131  disjss1f  32594  ssrelf  32637  axsepg2  35058  axsepg2ALT  35059  ss2mcls  35536  mclsax  35537  wzel  35788  onsuct0  36407  bj-zfauscl  36890  wl-ax13lem1  37460  axc11next  44375  traxext  44910  iscnrm3lem2  48614  setrec1lem2  48780