Theorem alrimdv 1930

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

Syntax hints:   → wi 4  ∀wal 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem is referenced by:  sbequ1  2253  ax13lem2  2378  reusv1  5340  zfpair  5364  axprlem3  5368  fliftfun  7256  isofrlem  7284  funcnvuni  7872  f1oweALT  7914  findcard  9086  findcard2  9087  dfac5lem4  10034  dfac5lem4OLD  10036  dfac5  10037  zorn2lem4  10407  genpcl  10917  psslinpr  10940  ltaddpr  10943  ltexprlem3  10947  suplem1pr  10961  uzwo  12822  seqf1o  13964  ramcl  16955  alexsubALTlem3  23991  bj-dvelimdv1  36996  intabssd  43702  frege81  44127  frege95  44141  frege123  44169  frege130  44176  truniALT  44724  ggen31  44728  onfrALTlem2  44729  gen21  44802  gen22  44805  ggen22  44806  relpfrlem  45136