Theorem alrimi 1515

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

Syntax hints:   → wi 4  ∀wal 1346  Ⅎwnf 1453

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-5 1440  ax-gen 1442  ax-4 1503

This theorem depends on definitions:  df-bi 116  df-nf 1454

This theorem is referenced by:  axc4i  1535  19.32r  1673  cbv3  1735  sbbid  1839  sbalyz  1992  dvelimdf  2009  dvelimor  2011  nf5d  2018  abbid  2287  nfcd  2307  nfabdw  2331  ralrimi  2541  r19.32r  2616  ceqsalg  2758  ceqsex  2768  vtocldf  2781  elrab3t  2885  morex  2914  sbciedf  2990  csbiebt  3088  csbiedf  3089  ssrd  3152  rgenm  3517  invdisj  3983  ssopab2b  4261  eusv2nf  4441  sniota  5189  imadif  5278  funimaexglem  5281  eusvobj1  5840  ssoprab2b  5910  ovmpodxf  5978