Theorem alrimdv 1857

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

Syntax hints:   → wi 4  ∀wal 1481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem is referenced by:  ax13lem2  2296  reusv1  4866  zfpair  4904  fliftfun  6562  isofrlem  6590  funcnvuni  7119  f1oweALT  7152  findcard  8199  findcard2  8200  dfac5lem4  8949  dfac5  8951  zorn2lem4  9321  genpcl  9830  psslinpr  9853  ltaddpr  9856  ltexprlem3  9860  suplem1pr  9874  uzwo  11751  seqf1o  12842  ramcl  15733  alexsubALTlem3  21853  bj-dvelimdv1  32835  intabssd  37916  frege81  38238  frege95  38252  frege123  38280  frege130  38287  truniALT  38751  ggen31  38760  onfrALTlem2  38761  gen21  38844  gen22  38847  ggen22  38848