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  5347  zfpair  5371  axprlem3  5375  fliftfun  7269  isofrlem  7297  funcnvuni  7888  f1oweALT  7930  findcard  9104  findcard2  9105  dfac5lem4  10055  dfac5lem4OLD  10057  dfac5  10058  zorn2lem4  10428  genpcl  10937  psslinpr  10960  ltaddpr  10963  ltexprlem3  10967  suplem1pr  10981  uzwo  12846  seqf1o  13984  ramcl  16976  alexsubALTlem3  23969  bj-dvelimdv1  36833  intabssd  43501  frege81  43926  frege95  43940  frege123  43968  frege130  43975  truniALT  44524  ggen31  44528  onfrALTlem2  44529  gen21  44602  gen22  44605  ggen22  44606  relpfrlem  44936