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 ⊢ (𝜑 → ∀𝑥𝜓)

This proof depends on syntax axioms:   → wi 4  ∀wal 1400  Ⅎwnf 1513

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1500  ax-gen 1502  ax-4 1563

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

This theorem is used 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  4123  ssopab2b  4419  eusv2nf  4602  sniota  5368  imadif  5461  funimaexglem  5464  eusvobj1  6072  ssoprab2b  6145  ovmpodxf  6214  modom  7108  nninfinf  10880