Theorem alrimdv 1930

Description: Deduction form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2207 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 1535

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  2249  ax13lem2  2394  reusv1  5300  zfpair  5324  fliftfun  7067  isofrlem  7095  funcnvuni  7638  f1oweALT  7675  findcard  8759  findcard2  8760  dfac5lem4  9554  dfac5  9556  zorn2lem4  9923  genpcl  10432  psslinpr  10455  ltaddpr  10458  ltexprlem3  10462  suplem1pr  10476  uzwo  12314  seqf1o  13414  ramcl  16367  alexsubALTlem3  22659  bj-dvelimdv1  34178  intabssd  39892  frege81  40297  frege95  40311  frege123  40339  frege130  40346  truniALT  40882  ggen31  40886  onfrALTlem2  40887  gen21  40960  gen22  40963  ggen22  40964