Theorem alrimdv 1936

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

Syntax hints:   → wi 4  ∀wal 1545

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem is referenced by:  sbequ1  2260  ax13lem2  2384  reusv1  5327  zfpair  5351  axprlem3  5355  fliftfun  7257  isofrlem  7285  funcnvuni  7873  f1oweALT  7915  findcard  9089  findcard2  9090  dfac5lem4  10040  dfac5lem4OLD  10042  dfac5  10043  zorn2lem4  10413  genpcl  10923  psslinpr  10946  ltaddpr  10949  ltexprlem3  10953  suplem1pr  10967  uzwo  12853  seqf1o  13997  ramcl  16992  alexsubALTlem3  24033  bj-dvelimdv1  37214  intabssd  43972  frege81  44397  frege95  44411  frege123  44439  frege130  44446  truniALT  44994  ggen31  44998  onfrALTlem2  44999  gen21  45072  gen22  45075  ggen22  45076  relpfrlem  45406