Theorem alrimdv 1956

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

Syntax hints:   → wi 4  ∀wal 1565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem is referenced by:  sbequ1  2290  ax13lem2  2414  reusv1  5369  zfpair  5393  axprlem3  5397  fliftfun  7311  isofrlem  7339  funcnvuni  7929  f1oweALT  7969  findcard  9148  findcard2  9149  dfac5lem4  10110  dfac5  10112  zorn2lem4  10483  genpcl  10993  psslinpr  11016  ltaddpr  11019  ltexprlem3  11023  suplem1pr  11037  uzwo  12935  seqf1o  14079  ramcl  17089  alexsubALTlem3  24175  bj-dvelimdv1  37410  intabssd  44171  frege81  44596  frege95  44610  frege123  44638  frege130  44645  truniALT  45176  ggen31  45180  onfrALTlem2  45181  gen21  45254  gen22  45257  ggen22  45258  relpfrlem  45588