Theorem alrimdv 1931

Description: Deduction form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2199 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 1538

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

This theorem is referenced by:  sbequ1  2239  ax13lem2  2374  reusv1  5395  zfpair  5419  fliftfun  7312  isofrlem  7340  funcnvuni  7925  f1oweALT  7962  findcard  9166  findcard2  9167  findcard2OLD  9287  dfac5lem4  10124  dfac5  10126  zorn2lem4  10497  genpcl  11006  psslinpr  11029  ltaddpr  11032  ltexprlem3  11036  suplem1pr  11050  uzwo  12900  seqf1o  14014  ramcl  16967  alexsubALTlem3  23774  bj-dvelimdv1  36035  intabssd  42573  frege81  42998  frege95  43012  frege123  43040  frege130  43047  truniALT  43605  ggen31  43609  onfrALTlem2  43610  gen21  43683  gen22  43686  ggen22  43687