Theorem alrimdv 1931

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

Syntax hints:   → wi 4  ∀wal 1540

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

This theorem is referenced by:  sbequ1  2256  ax13lem2  2381  reusv1  5332  zfpair  5356  axprlem3  5360  fliftfun  7258  isofrlem  7286  funcnvuni  7874  f1oweALT  7916  findcard  9089  findcard2  9090  dfac5lem4  10037  dfac5lem4OLD  10039  dfac5  10040  zorn2lem4  10410  genpcl  10920  psslinpr  10943  ltaddpr  10946  ltexprlem3  10950  suplem1pr  10964  uzwo  12825  seqf1o  13967  ramcl  16958  alexsubALTlem3  23992  bj-dvelimdv1  37157  intabssd  43949  frege81  44374  frege95  44388  frege123  44416  frege130  44423  truniALT  44971  ggen31  44975  onfrALTlem2  44976  gen21  45049  gen22  45052  ggen22  45053  relpfrlem  45383