Theorem alrimi 1571

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

Syntax hints:   → wi 4  ∀wal 1396  Ⅎwnf 1509

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1496  ax-gen 1498  ax-4 1559

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

This theorem is referenced by:  axc4i  1591  19.32r  1728  cbv3  1791  sbbid  1895  sbalyz  2055  dvelimdf  2072  dvelimor  2074  nf5d  2081  abbid  2351  nfcd  2381  nfabdw  2405  ralrimi  2615  r19.32r  2691  ceqsalg  2844  ceqsex  2854  vtocldf  2868  elrab3t  2975  morex  3004  sbciedf  3081  csbiebt  3181  csbiedf  3182  ssrd  3247  invdisj  4107  ssopab2b  4400  eusv2nf  4582  sniota  5348  imadif  5441  funimaexglem  5444  eusvobj1  6045  ssoprab2b  6118  ovmpodxf  6187  modom  7074  nninfinf  10829