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  2828  ceqsex  2838  vtocldf  2852  elrab3t  2958  morex  2987  sbciedf  3064  csbiebt  3164  csbiedf  3165  ssrd  3229  invdisj  4075  ssopab2b  4364  eusv2nf  4546  sniota  5308  imadif  5400  funimaexglem  5403  eusvobj1  5987  ssoprab2b  6060  ovmpodxf  6129  nninfinf  10660