Theorem alrimdv 1926

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

Syntax hints:   → wi 4  ∀wal 1531

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

This theorem is referenced by:  sbequ1  2245  ax13lem2  2390  reusv1  5289  zfpair  5313  fliftfun  7059  isofrlem  7087  funcnvuni  7630  f1oweALT  7667  findcard  8751  findcard2  8752  dfac5lem4  9546  dfac5  9548  zorn2lem4  9915  genpcl  10424  psslinpr  10447  ltaddpr  10450  ltexprlem3  10454  suplem1pr  10468  uzwo  12305  seqf1o  13405  ramcl  16359  alexsubALTlem3  22651  bj-dvelimdv1  34171  intabssd  39878  frege81  40283  frege95  40297  frege123  40325  frege130  40332  truniALT  40868  ggen31  40872  onfrALTlem2  40873  gen21  40946  gen22  40949  ggen22  40950