Theorem alimdv 1911

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

Syntax hints:   → wi 4  ∀wal 1531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1789  ax-4 1803  ax-5 1905

This theorem is referenced by:  2alimdv  1913  ax12v2  2165  ax13lem1  2365  axc16i  2427  mo4  2552  ralimdv2  3155  mo2icl  3703  sstr2  3982  reuss2  4308  ssuni  4927  disjss2  5107  disjss1  5110  disjiun  5126  disjss3  5138  alxfr  5396  axprlem1  5412  axprlem2  5413  axpr  5417  frss  5634  ssrel  5773  ssrelOLD  5774  ssrel2  5776  ssrelrel  5787  iotavalOLD  6508  fvn0ssdmfun  7067  dff3  7092  dfwe2  7755  trom  7858  findcard3  9282  findcard3OLD  9283  dffi2  9415  indcardi  10033  zorn2lem4  10491  uzindi  13945  caubnd  15303  ramtlecl  16934  psgnunilem4  19409  nrhmzr  20429  dfconn2  23247  wilthlem3  26921  disjss1f  32275  ssrelf  32316  ss2mcls  35050  mclsax  35051  wzel  35292  onsuct0  35817  bj-zfauscl  36295  wl-ax13lem1  36866  axc11next  43679  iscnrm3lem2  47779  setrec1lem2  47945