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  5346  zfpair  5370  axprlem3  5374  fliftfun  7270  isofrlem  7298  funcnvuni  7886  f1oweALT  7928  findcard  9102  findcard2  9103  dfac5lem4  10050  dfac5lem4OLD  10052  dfac5  10053  zorn2lem4  10423  genpcl  10933  psslinpr  10956  ltaddpr  10959  ltexprlem3  10963  suplem1pr  10977  uzwo  12838  seqf1o  13980  ramcl  16971  alexsubALTlem3  24010  bj-dvelimdv1  37127  intabssd  43904  frege81  44329  frege95  44343  frege123  44371  frege130  44378  truniALT  44926  ggen31  44930  onfrALTlem2  44931  gen21  45004  gen22  45007  ggen22  45008  relpfrlem  45338