Theorem alrimi 1568

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

Syntax hints:   → wi 4  ∀wal 1393  Ⅎwnf 1506

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1493  ax-gen 1495  ax-4 1556

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

This theorem is referenced by:  axc4i  1588  19.32r  1726  cbv3  1788  sbbid  1892  sbalyz  2050  dvelimdf  2067  dvelimor  2069  nf5d  2076  abbid  2346  nfcd  2367  nfabdw  2391  ralrimi  2601  r19.32r  2677  ceqsalg  2829  ceqsex  2839  vtocldf  2853  elrab3t  2959  morex  2988  sbciedf  3065  csbiebt  3165  csbiedf  3166  ssrd  3230  invdisj  4079  ssopab2b  4369  eusv2nf  4551  sniota  5315  imadif  5407  funimaexglem  5410  eusvobj1  6000  ssoprab2b  6073  ovmpodxf  6142  modom  6989  nninfinf  10695