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  2380  reusv1  5339  zfpair  5363  axprlem3  5367  fliftfun  7267  isofrlem  7295  funcnvuni  7883  f1oweALT  7925  findcard  9098  findcard2  9099  dfac5lem4  10048  dfac5lem4OLD  10050  dfac5  10051  zorn2lem4  10421  genpcl  10931  psslinpr  10954  ltaddpr  10957  ltexprlem3  10961  suplem1pr  10975  uzwo  12861  seqf1o  14005  ramcl  17000  alexsubALTlem3  24014  bj-dvelimdv1  37159  intabssd  43946  frege81  44371  frege95  44385  frege123  44413  frege130  44420  truniALT  44968  ggen31  44972  onfrALTlem2  44973  gen21  45046  gen22  45049  ggen22  45050  relpfrlem  45380