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  2053  dvelimdf  2070  dvelimor  2072  nf5d  2079  abbid  2349  nfcd  2379  nfabdw  2403  ralrimi  2613  r19.32r  2689  ceqsalg  2842  ceqsex  2852  vtocldf  2866  elrab3t  2972  morex  3001  sbciedf  3078  csbiebt  3178  csbiedf  3179  ssrd  3243  invdisj  4102  ssopab2b  4395  eusv2nf  4577  sniota  5343  imadif  5436  funimaexglem  5439  eusvobj1  6037  ssoprab2b  6110  ovmpodxf  6179  modom  7061  nninfinf  10805