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  2381  reusv1  5372  zfpair  5396  axprlem3  5400  fliftfun  7310  isofrlem  7338  funcnvuni  7933  f1oweALT  7976  findcard  9182  findcard2  9183  dfac5lem4  10145  dfac5lem4OLD  10147  dfac5  10148  zorn2lem4  10518  genpcl  11027  psslinpr  11050  ltaddpr  11053  ltexprlem3  11057  suplem1pr  11071  uzwo  12932  seqf1o  14066  ramcl  17054  alexsubALTlem3  23992  bj-dvelimdv1  36875  intabssd  43510  frege81  43935  frege95  43949  frege123  43977  frege130  43984  truniALT  44533  ggen31  44537  onfrALTlem2  44538  gen21  44611  gen22  44614  ggen22  44615  relpfrlem  44945