Theorem alrimdv 1962

Description: Deduction form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2243 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  2283  ax13lem2  2405  reusv1  5362  zfpair  5386  axprlem3  5390  fliftfun  7314  isofrlem  7342  funcnvuni  7930  f1oweALT  7970  findcard  9161  findcard2  9162  dfac5lem4  10132  dfac5  10134  zorn2lem4  10504  genpcl  11020  psslinpr  11043  ltaddpr  11046  ltexprlem3  11050  suplem1pr  11064  uzwo  12963  seqf1o  14110  ramcl  17124  alexsubALTlem3  24278  bj-dvelimdv1  37598  intabssd  44362  frege81  44787  frege95  44801  frege123  44829  frege130  44836  truniALT  45367  ggen31  45371  onfrALTlem2  45372  gen21  45445  gen22  45448  ggen22  45449  relpfrlem  45779