Theorem alrimi 1575

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

Syntax hints:   → wi 4  ∀wal 1400  Ⅎwnf 1513

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1500  ax-gen 1502  ax-4 1563

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

This theorem is referenced by:  axc4i  1595  19.32r  1732  cbv3  1795  sbbid  1899  sbalyz  2059  dvelimdf  2076  dvelimor  2078  nf5d  2085  abbid  2355  nfcd  2387  nfabdw  2411  ralrimi  2621  r19.32r  2697  ceqsalg  2850  ceqsex  2860  vtocldf  2874  elrab3t  2981  morex  3010  sbciedf  3087  csbiebt  3187  csbiedf  3188  ssrd  3253  invdisj  4118  ssopab2b  4414  eusv2nf  4597  sniota  5363  imadif  5456  funimaexglem  5459  eusvobj1  6062  ssoprab2b  6135  ovmpodxf  6204  modom  7098  nninfinf  10858