Theorem alrimdv 1932

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

Syntax hints:   → wi 4  ∀wal 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1798  ax-4 1812  ax-5 1913

This theorem is referenced by:  sbequ1  2240  ax13lem2  2376  reusv1  5320  zfpair  5344  fliftfun  7183  isofrlem  7211  funcnvuni  7778  f1oweALT  7815  findcard  8946  findcard2  8947  findcard2OLD  9056  dfac5lem4  9882  dfac5  9884  zorn2lem4  10255  genpcl  10764  psslinpr  10787  ltaddpr  10790  ltexprlem3  10794  suplem1pr  10808  uzwo  12651  seqf1o  13764  ramcl  16730  alexsubALTlem3  23200  bj-dvelimdv1  35036  intabssd  41126  frege81  41552  frege95  41566  frege123  41594  frege130  41601  truniALT  42161  ggen31  42165  onfrALTlem2  42166  gen21  42239  gen22  42242  ggen22  42243