Theorem alrimi 1546

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)

Hypotheses

Ref	Expression
alrimi.1	⊢ Ⅎ𝑥𝜑
alrimi.2	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
alrimi	⊢ (𝜑 → ∀𝑥𝜓)

Proof of Theorem alrimi

Step	Hyp	Ref	Expression
1		alrimi.1	. . 3 ⊢ Ⅎ𝑥𝜑
2	1	nfri 1543	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
3		alrimi.2	. 2 ⊢ (𝜑 → 𝜓)
4	2, 3	alrimih 1493	1 ⊢ (𝜑 → ∀𝑥𝜓)

Syntax hints:   → wi 4  ∀wal 1371  Ⅎwnf 1484

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1471  ax-gen 1473  ax-4 1534

This theorem depends on definitions:  df-bi 117  df-nf 1485

This theorem is referenced by:  axc4i  1566  19.32r  1704  cbv3  1766  sbbid  1870  sbalyz  2028  dvelimdf  2045  dvelimor  2047  nf5d  2054  abbid  2324  nfcd  2345  nfabdw  2369  ralrimi  2579  r19.32r  2654  ceqsalg  2805  ceqsex  2815  vtocldf  2829  elrab3t  2935  morex  2964  sbciedf  3041  csbiebt  3141  csbiedf  3142  ssrd  3206  invdisj  4052  ssopab2b  4341  eusv2nf  4521  sniota  5281  imadif  5373  funimaexglem  5376  eusvobj1  5954  ssoprab2b  6025  ovmpodxf  6094  nninfinf  10625