Theorem alrimi 1502

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

Syntax hints:   → wi 4  ∀wal 1333  Ⅎwnf 1440

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-5 1427  ax-gen 1429  ax-4 1490

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

This theorem is referenced by:  axc4i  1522  19.32r  1660  cbv3  1722  sbbid  1826  sbalyz  1979  dvelimdf  1996  dvelimor  1998  nf5d  2005  abbid  2274  nfcd  2294  nfabdw  2318  ralrimi  2528  r19.32r  2603  ceqsalg  2740  ceqsex  2750  vtocldf  2763  elrab3t  2867  morex  2896  sbciedf  2972  csbiebt  3070  csbiedf  3071  ssrd  3133  rgenm  3496  invdisj  3959  ssopab2b  4236  eusv2nf  4416  sniota  5162  imadif  5250  funimaexglem  5253  eusvobj1  5811  ssoprab2b  5878  ovmpodxf  5946