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  5336  zfpair  5360  axprlem3  5364  fliftfun  7262  isofrlem  7290  funcnvuni  7878  f1oweALT  7920  findcard  9093  findcard2  9094  dfac5lem4  10043  dfac5lem4OLD  10045  dfac5  10046  zorn2lem4  10416  genpcl  10926  psslinpr  10949  ltaddpr  10952  ltexprlem3  10956  suplem1pr  10970  uzwo  12856  seqf1o  14000  ramcl  16995  alexsubALTlem3  24028  bj-dvelimdv1  37179  intabssd  43968  frege81  44393  frege95  44407  frege123  44435  frege130  44442  truniALT  44990  ggen31  44994  onfrALTlem2  44995  gen21  45068  gen22  45071  ggen22  45072  relpfrlem  45402