Theorem alrimi 1570

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

Syntax hints:   → wi 4  ∀wal 1395  Ⅎwnf 1508

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1495  ax-gen 1497  ax-4 1558

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

This theorem is referenced by:  axc4i  1590  19.32r  1728  cbv3  1790  sbbid  1894  sbalyz  2052  dvelimdf  2069  dvelimor  2071  nf5d  2078  abbid  2348  nfcd  2369  nfabdw  2393  ralrimi  2603  r19.32r  2679  ceqsalg  2831  ceqsex  2841  vtocldf  2855  elrab3t  2961  morex  2990  sbciedf  3067  csbiebt  3167  csbiedf  3168  ssrd  3232  invdisj  4081  ssopab2b  4371  eusv2nf  4553  sniota  5317  imadif  5410  funimaexglem  5413  eusvobj1  6004  ssoprab2b  6077  ovmpodxf  6146  modom  6993  nninfinf  10704