Theorem alrimi 2249

Description: Inference form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2243. (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	nf5ri 2231	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
3		alrimi.2	. 2 ⊢ (𝜑 → 𝜓)
4	2, 3	alrimih 1857	1 ⊢ (𝜑 → ∀𝑥𝜓)

This proof depends on syntax axioms:   → wi 4  ∀wal 1568  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2213

This proof depends on definitions:  df-bi 210  df-ex 1813  df-nf 1817

This theorem is used by:  sbalex  2278  sbimd  2280  sbbid  2281  nf5d  2317  axc4i  2352  19.12  2357  nfsbd  2551  mobid  2575  mo3  2589  eubid  2612  2moexv  2652  eupicka  2659  2moex  2665  2mo  2673  abbid  2828  nfcd  2915  ceqsalgALT  3486  vtocldf  3521  rspcdf  3563  elrab3t  3644  morex  3677  sbciedf  3781  csbiebt  3876  csbiedf  3877  ssrd  3936  eqrd  3950  invdisj  5089  zfrepclf  5246  eusv2nf  5360  ssopab2bw  5526  ssopab2b  5528  imadif  6618  eusvobj1  7407  ssoprab2b  7483  eqoprab2bw  7484  ovmpodxf  7564  axrepnd  10606  axunnd  10608  axpownd  10613  axregndlem1  10614  axacndlem1  10619  axacndlem2  10620  axacndlem3  10621  axacndlem4  10622  axacndlem5  10623  axacnd  10624  mreexexd  17739  acsmapd  18645  isch3  31725  ssrelf  33091  eqrelrd2  33092  esumeq12dvaf  34544  bnj1366  35341  bnj571  35418  bnj964  35455  iota5f  36306  axtcond  37100  bj-nfext  37450  wl-mo3t  38342  cover2  38468  alrimii  38870  mpobi123f  38913  mptbi12f  38917  ss2iundf  44502  pm11.57  45216  pm11.59  45218  tratrb  45362  hbexg  45382  e2ebindALT  45754  modelaxreplem2  45805  permaxrep  45832  dvnmul  46774  stoweidlem34  46865  sge0fodjrnlem  47247  pimrecltpos  47539  pimrecltneg  47555  smfaddlem1  47594  smfresal  47619  smfinflem  47648  ichnfim  48367  ovmpordxf  49272  setrec1lem4  50619