Theorem alrimdv 1930

Description: Deduction form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2205 and 19.21v 1940. (Contributed by NM, 10-Feb-1997.)

Hypothesis

Ref	Expression
alrimdv.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
alrimdv	⊢ (𝜑 → (𝜓 → ∀𝑥𝜒))

Distinct variable groups:   𝜑,𝑥   𝜓,𝑥

Allowed substitution hint:   𝜒(𝑥)

Proof of Theorem alrimdv

Step	Hyp	Ref	Expression
1		ax-5 1911	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		ax-5 1911	. 2 ⊢ (𝜓 → ∀𝑥𝜓)
3		alrimdv.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 2, 3	alrimdh 1864	1 ⊢ (𝜑 → (𝜓 → ∀𝑥𝜒))

Syntax hints:   → wi 4  ∀wal 1536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1797  ax-4 1811  ax-5 1911

This theorem is referenced by:  sbequ1  2246  ax13lem2  2383  reusv1  5263  zfpair  5287  fliftfun  7044  isofrlem  7072  funcnvuni  7618  f1oweALT  7655  findcard  8741  findcard2  8742  dfac5lem4  9537  dfac5  9539  zorn2lem4  9910  genpcl  10419  psslinpr  10442  ltaddpr  10445  ltexprlem3  10449  suplem1pr  10463  uzwo  12299  seqf1o  13407  ramcl  16355  alexsubALTlem3  22654  bj-dvelimdv1  34291  intabssd  40227  frege81  40645  frege95  40659  frege123  40687  frege130  40694  truniALT  41247  ggen31  41251  onfrALTlem2  41252  gen21  41325  gen22  41328  ggen22  41329