Theorem alrimdv 1928

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

Syntax hints:   → wi 4  ∀wal 1535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem is referenced by:  sbequ1  2249  ax13lem2  2384  reusv1  5415  zfpair  5439  fliftfun  7348  isofrlem  7376  funcnvuni  7972  f1oweALT  8013  findcard  9229  findcard2  9230  dfac5lem4  10195  dfac5lem4OLD  10197  dfac5  10198  zorn2lem4  10568  genpcl  11077  psslinpr  11100  ltaddpr  11103  ltexprlem3  11107  suplem1pr  11121  uzwo  12976  seqf1o  14094  ramcl  17076  alexsubALTlem3  24078  bj-dvelimdv1  36818  intabssd  43481  frege81  43906  frege95  43920  frege123  43948  frege130  43955  truniALT  44512  ggen31  44516  onfrALTlem2  44517  gen21  44590  gen22  44593  ggen22  44594