Theorem alrimdv 1929

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

Syntax hints:   → wi 4  ∀wal 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem is referenced by:  sbequ1  2249  ax13lem2  2374  reusv1  5336  zfpair  5360  axprlem3  5364  fliftfun  7249  isofrlem  7277  funcnvuni  7865  f1oweALT  7907  findcard  9077  findcard2  9078  dfac5lem4  10020  dfac5lem4OLD  10022  dfac5  10023  zorn2lem4  10393  genpcl  10902  psslinpr  10925  ltaddpr  10928  ltexprlem3  10932  suplem1pr  10946  uzwo  12812  seqf1o  13950  ramcl  16941  alexsubALTlem3  23934  bj-dvelimdv1  36836  intabssd  43502  frege81  43927  frege95  43941  frege123  43969  frege130  43976  truniALT  44525  ggen31  44529  onfrALTlem2  44530  gen21  44603  gen22  44606  ggen22  44607  relpfrlem  44937