Theorem alrimi 1544

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

Syntax hints:   → wi 4  ∀wal 1370  Ⅎwnf 1482

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

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

This theorem is referenced by:  axc4i  1564  19.32r  1702  cbv3  1764  sbbid  1868  sbalyz  2026  dvelimdf  2043  dvelimor  2045  nf5d  2052  abbid  2321  nfcd  2342  nfabdw  2366  ralrimi  2576  r19.32r  2651  ceqsalg  2799  ceqsex  2809  vtocldf  2823  elrab3t  2927  morex  2956  sbciedf  3033  csbiebt  3132  csbiedf  3133  ssrd  3197  invdisj  4037  ssopab2b  4322  eusv2nf  4502  sniota  5261  imadif  5353  funimaexglem  5356  eusvobj1  5930  ssoprab2b  6001  ovmpodxf  6070  nninfinf  10586