Theorem alrimdv 1963

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1827  ax-4 1841  ax-5 1944

This theorem is used by:  sbequ1  2286  ax13lem2  2408  reusv1  5363  zfpair  5387  axprlem3  5391  fliftfun  7330  isofrlem  7358  funcnvuni  7954  f1oweALT  7994  findcard  9193  findcard2  9194  dfac5lem4  10218  dfac5  10220  zorn2lem4  10590  genpcl  11106  psslinpr  11129  ltaddpr  11132  ltexprlem3  11136  suplem1pr  11150  uzwo  13051  seqf1o  14199  ramcl  17222  alexsubALTlem3  24383  bj-dvelimdv1  37897  intabssd  44666  frege81  45090  frege95  45104  frege123  45132  frege130  45139  truniALT  45669  ggen31  45673  onfrALTlem2  45674  gen21  45747  gen22  45750  ggen22  45751  relpfrlem  46088