Theorem alrimdv 1962

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1828  ax-4 1842  ax-5 1943

This theorem is used by:  sbequ1  2284  ax13lem2  2406  reusv1  5359  zfpair  5383  axprlem3  5387  fliftfun  7320  isofrlem  7348  funcnvuni  7944  f1oweALT  7984  findcard  9179  findcard2  9180  dfac5lem4  10205  dfac5  10207  zorn2lem4  10577  genpcl  11093  psslinpr  11116  ltaddpr  11119  ltexprlem3  11123  suplem1pr  11137  uzwo  13038  seqf1o  14186  ramcl  17207  alexsubALTlem3  24368  bj-dvelimdv1  37764  intabssd  44519  frege81  44943  frege95  44957  frege123  44985  frege130  44992  truniALT  45523  ggen31  45527  onfrALTlem2  45528  gen21  45601  gen22  45604  ggen22  45605  relpfrlem  45942