Theorem alrimi 1467

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

Syntax hints:   → wi 4  ∀wal 1294  Ⅎwnf 1401

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-5 1388  ax-gen 1390  ax-4 1452

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

This theorem is referenced by:  19.32r  1622  cbv3  1684  sbbid  1781  sbalyz  1930  dvelimdf  1947  dvelimor  1949  abbid  2211  nfcd  2230  ralrimi  2456  r19.32r  2528  ceqsalg  2661  ceqsex  2671  vtocldf  2684  elrab3t  2784  morex  2813  sbciedf  2888  csbiebt  2981  csbiedf  2982  ssrd  3044  rgenm  3404  invdisj  3861  ssopab2b  4127  eusv2nf  4306  sniota  5041  imadif  5128  funimaexglem  5131  eusvobj1  5677  ssoprab2b  5744  ovmpt2dxf  5808