Theorem alrimdv 1962

Description: Deduction form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2246 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  2286  ax13lem2  2410  reusv1  5370  zfpair  5394  axprlem3  5398  fliftfun  7319  isofrlem  7347  funcnvuni  7935  f1oweALT  7975  findcard  9155  findcard2  9156  dfac5lem4  10126  dfac5  10128  zorn2lem4  10498  genpcl  11012  psslinpr  11035  ltaddpr  11038  ltexprlem3  11042  suplem1pr  11056  uzwo  12955  seqf1o  14101  ramcl  17115  alexsubALTlem3  24261  bj-dvelimdv1  37548  intabssd  44322  frege81  44747  frege95  44761  frege123  44789  frege130  44796  truniALT  45327  ggen31  45331  onfrALTlem2  45332  gen21  45405  gen22  45408  ggen22  45409  relpfrlem  45739