Theorem alrimdv 1930

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

Syntax hints:   → wi 4  ∀wal 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem is referenced by:  sbequ1  2251  ax13lem2  2376  reusv1  5333  zfpair  5357  axprlem3  5361  fliftfun  7246  isofrlem  7274  funcnvuni  7862  f1oweALT  7904  findcard  9073  findcard2  9074  dfac5lem4  10017  dfac5lem4OLD  10019  dfac5  10020  zorn2lem4  10390  genpcl  10899  psslinpr  10922  ltaddpr  10925  ltexprlem3  10929  suplem1pr  10943  uzwo  12809  seqf1o  13950  ramcl  16941  alexsubALTlem3  23964  bj-dvelimdv1  36896  intabssd  43622  frege81  44047  frege95  44061  frege123  44089  frege130  44096  truniALT  44644  ggen31  44648  onfrALTlem2  44649  gen21  44722  gen22  44725  ggen22  44726  relpfrlem  45056