Theorem alrimdv 1888

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

Syntax hints:   → wi 4  ∀wal 1505

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1758  ax-4 1772  ax-5 1869

This theorem is referenced by:  sbequ1  2174  ax13lem2  2303  moexexvw  2656  reusv1  5145  zfpair  5172  fliftfun  6882  isofrlem  6910  funcnvuni  7445  f1oweALT  7478  findcard  8544  findcard2  8545  dfac5lem4  9338  dfac5  9340  zorn2lem4  9711  genpcl  10220  psslinpr  10243  ltaddpr  10246  ltexprlem3  10250  suplem1pr  10264  uzwo  12118  seqf1o  13219  ramcl  16211  alexsubALTlem3  22351  bj-dvelimdv1  33607  intabssd  39277  frege81  39598  frege95  39612  frege123  39640  frege130  39647  truniALT  40238  ggen31  40242  onfrALTlem2  40243  gen21  40316  gen22  40319  ggen22  40320