Theorem alrimi 1503

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

Syntax hints:   → wi 4  ∀wal 1330  Ⅎwnf 1437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-5 1424  ax-gen 1426  ax-4 1488

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

This theorem is referenced by:  19.32r  1659  cbv3  1721  sbbid  1819  sbalyz  1975  dvelimdf  1992  dvelimor  1994  abbid  2257  nfcd  2277  ralrimi  2506  r19.32r  2581  ceqsalg  2717  ceqsex  2727  vtocldf  2740  elrab3t  2843  morex  2872  sbciedf  2948  csbiebt  3044  csbiedf  3045  ssrd  3107  rgenm  3470  invdisj  3931  ssopab2b  4206  eusv2nf  4385  sniota  5123  imadif  5211  funimaexglem  5214  eusvobj1  5769  ssoprab2b  5836  ovmpodxf  5904