Theorem alrimdv 1931

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

Syntax hints:   → wi 4  ∀wal 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem is referenced by:  sbequ1  2256  ax13lem2  2381  reusv1  5343  zfpair  5367  axprlem3  5371  fliftfun  7260  isofrlem  7288  funcnvuni  7876  f1oweALT  7918  findcard  9092  findcard2  9093  dfac5lem4  10040  dfac5lem4OLD  10042  dfac5  10043  zorn2lem4  10413  genpcl  10923  psslinpr  10946  ltaddpr  10949  ltexprlem3  10953  suplem1pr  10967  uzwo  12828  seqf1o  13970  ramcl  16961  alexsubALTlem3  23997  bj-dvelimdv1  37055  intabssd  43827  frege81  44252  frege95  44266  frege123  44294  frege130  44301  truniALT  44849  ggen31  44853  onfrALTlem2  44854  gen21  44927  gen22  44930  ggen22  44931  relpfrlem  45261