Theorem alrimdv 1844

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

Syntax hints:   → wi 4  ∀wal 1473

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1713  ax-4 1728  ax-5 1827

This theorem is referenced by:  ax13lem2  2284  reusv1  4792  zfpair  4831  fliftfun  6462  isofrlem  6490  funcnvuni  7012  f1oweALT  7043  findcard  8084  findcard2  8085  dfac5lem4  8832  dfac5  8834  zorn2lem4  9204  genpcl  9709  psslinpr  9732  ltaddpr  9735  ltexprlem3  9739  suplem1pr  9753  uzwo  11627  seqf1o  12704  ramcl  15571  alexsubALTlem3  21663  bj-dvelimdv1  32028  intabssd  36935  frege81  37258  frege95  37272  frege123  37300  frege130  37307  truniALT  37772  ggen31  37781  onfrALTlem2  37782  gen21  37865  gen22  37868  ggen22  37869