Theorem alrimi 1545

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

Syntax hints:   → wi 4  ∀wal 1371  Ⅎwnf 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1470  ax-gen 1472  ax-4 1533

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

This theorem is referenced by:  axc4i  1565  19.32r  1703  cbv3  1765  sbbid  1869  sbalyz  2027  dvelimdf  2044  dvelimor  2046  nf5d  2053  abbid  2322  nfcd  2343  nfabdw  2367  ralrimi  2577  r19.32r  2652  ceqsalg  2800  ceqsex  2810  vtocldf  2824  elrab3t  2928  morex  2957  sbciedf  3034  csbiebt  3133  csbiedf  3134  ssrd  3198  invdisj  4038  ssopab2b  4323  eusv2nf  4503  sniota  5262  imadif  5354  funimaexglem  5357  eusvobj1  5931  ssoprab2b  6002  ovmpodxf  6071  nninfinf  10588