Theorem alrimdv 1933

Description: Deduction form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2203 and 19.21v 1943. (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 1914	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		ax-5 1914	. 2 ⊢ (𝜓 → ∀𝑥𝜓)
3		alrimdv.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 2, 3	alrimdh 1867	1 ⊢ (𝜑 → (𝜓 → ∀𝑥𝜒))

Syntax hints:   → wi 4  ∀wal 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem is referenced by:  sbequ1  2243  ax13lem2  2376  reusv1  5315  zfpair  5339  fliftfun  7163  isofrlem  7191  funcnvuni  7752  f1oweALT  7788  findcard  8908  findcard2  8909  findcard2OLD  8986  dfac5lem4  9813  dfac5  9815  zorn2lem4  10186  genpcl  10695  psslinpr  10718  ltaddpr  10721  ltexprlem3  10725  suplem1pr  10739  uzwo  12580  seqf1o  13692  ramcl  16658  alexsubALTlem3  23108  bj-dvelimdv1  34963  intabssd  41024  frege81  41441  frege95  41455  frege123  41483  frege130  41490  truniALT  42050  ggen31  42054  onfrALTlem2  42055  gen21  42128  gen22  42131  ggen22  42132