Theorem alrimdv 1959

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

This theorem is used by:  sbequ1  2284  ax13lem2  2408  reusv1  5368  zfpair  5392  axprlem3  5396  fliftfun  7310  isofrlem  7338  funcnvuni  7925  f1oweALT  7965  findcard  9144  findcard2  9145  dfac5lem4  10115  dfac5  10117  zorn2lem4  10487  genpcl  10997  psslinpr  11020  ltaddpr  11023  ltexprlem3  11027  suplem1pr  11041  uzwo  12939  seqf1o  14084  ramcl  17093  alexsubALTlem3  24215  bj-dvelimdv1  37515  intabssd  44273  frege81  44698  frege95  44712  frege123  44740  frege130  44747  truniALT  45278  ggen31  45282  onfrALTlem2  45283  gen21  45356  gen22  45359  ggen22  45360  relpfrlem  45690