Theorem alrimdv 1950

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

Syntax hints:   → wi 4  ∀wal 1559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1816  ax-4 1830  ax-5 1931

This theorem is referenced by:  sbequ1  2284  ax13lem2  2408  reusv1  5355  zfpair  5379  axprlem3  5383  fliftfun  7297  isofrlem  7325  funcnvuni  7914  f1oweALT  7954  findcard  9133  findcard2  9134  dfac5lem4  10083  dfac5lem4OLD  10085  dfac5  10086  zorn2lem4  10457  genpcl  10967  psslinpr  10990  ltaddpr  10993  ltexprlem3  10997  suplem1pr  11011  uzwo  12913  seqf1o  14057  ramcl  17066  alexsubALTlem3  24110  bj-dvelimdv1  37338  intabssd  44096  frege81  44521  frege95  44535  frege123  44563  frege130  44570  truniALT  45118  ggen31  45122  onfrALTlem2  45123  gen21  45196  gen22  45199  ggen22  45200  relpfrlem  45530