Theorem alrimi 1571

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 1568	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
3		alrimi.2	. 2 ⊢ (𝜑 → 𝜓)
4	2, 3	alrimih 1518	1 ⊢ (𝜑 → ∀𝑥𝜓)

Syntax hints:   → wi 4  ∀wal 1396  Ⅎwnf 1509

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1496  ax-gen 1498  ax-4 1559

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

This theorem is referenced by:  axc4i  1591  19.32r  1728  cbv3  1790  sbbid  1894  sbalyz  2052  dvelimdf  2069  dvelimor  2071  nf5d  2078  abbid  2348  nfcd  2370  nfabdw  2394  ralrimi  2604  r19.32r  2680  ceqsalg  2832  ceqsex  2842  vtocldf  2856  elrab3t  2962  morex  2991  sbciedf  3068  csbiebt  3168  csbiedf  3169  ssrd  3233  invdisj  4086  ssopab2b  4377  eusv2nf  4559  sniota  5324  imadif  5417  funimaexglem  5420  eusvobj1  6015  ssoprab2b  6088  ovmpodxf  6157  modom  7037  nninfinf  10751