Theorem alrimdv 1929

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

Syntax hints:   → wi 4  ∀wal 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem is referenced by:  sbequ1  2249  ax13lem2  2374  reusv1  5352  zfpair  5376  axprlem3  5380  fliftfun  7287  isofrlem  7315  funcnvuni  7908  f1oweALT  7951  findcard  9127  findcard2  9128  dfac5lem4  10079  dfac5lem4OLD  10081  dfac5  10082  zorn2lem4  10452  genpcl  10961  psslinpr  10984  ltaddpr  10987  ltexprlem3  10991  suplem1pr  11005  uzwo  12870  seqf1o  14008  ramcl  17000  alexsubALTlem3  23936  bj-dvelimdv1  36840  intabssd  43508  frege81  43933  frege95  43947  frege123  43975  frege130  43982  truniALT  44531  ggen31  44535  onfrALTlem2  44536  gen21  44609  gen22  44612  ggen22  44613  relpfrlem  44943