Theorem alrimdv 1927

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

Syntax hints:   → wi 4  ∀wal 1535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1792  ax-4 1806  ax-5 1908

This theorem is referenced by:  sbequ1  2246  ax13lem2  2379  reusv1  5403  zfpair  5427  axprlem3  5431  fliftfun  7332  isofrlem  7360  funcnvuni  7955  f1oweALT  7996  findcard  9202  findcard2  9203  dfac5lem4  10164  dfac5lem4OLD  10166  dfac5  10167  zorn2lem4  10537  genpcl  11046  psslinpr  11069  ltaddpr  11072  ltexprlem3  11076  suplem1pr  11090  uzwo  12951  seqf1o  14081  ramcl  17063  alexsubALTlem3  24073  bj-dvelimdv1  36835  intabssd  43509  frege81  43934  frege95  43948  frege123  43976  frege130  43983  truniALT  44539  ggen31  44543  onfrALTlem2  44544  gen21  44617  gen22  44620  ggen22  44621