Theorem alrimi 2250

Description: Inference form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2244. (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 2232	. 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  2279  sbimd  2281  sbbid  2282  nf5d  2318  axc4i  2353  19.12  2358  nfsbd  2552  mobid  2576  mo3  2590  eubid  2613  2moexv  2653  eupicka  2660  2moex  2666  2mo  2674  abbid  2829  nfcd  2916  ceqsalgALT  3487  vtocldf  3522  rspcdf  3564  elrab3t  3644  morex  3677  sbciedf  3781  csbiebt  3876  csbiedf  3877  ssrd  3936  eqrd  3950  invdisj  5089  zfrepclf  5244  eusv2nf  5357  ssopab2bw  5522  ssopab2b  5524  imadif  6624  eusvobj1  7413  ssoprab2b  7489  eqoprab2bw  7490  ovmpodxf  7570  setrec1lem4  9971  axrepnd  10679  axunnd  10681  axpownd  10686  axregndlem1  10687  axacndlem1  10692  axacndlem2  10693  axacndlem3  10694  axacndlem4  10695  axacndlem5  10696  axacnd  10697  mreexexd  17822  acsmapd  18728  isch3  31843  ssrelf  33209  eqrelrd2  33210  esumeq12dvaf  34663  bnj1366  35459  bnj571  35536  bnj964  35573  iota5f  36489  axtcond  37266  bj-nfext  37616  wl-mo3t  38508  cover2  38649  alrimii  39051  mpobi123f  39094  mptbi12f  39098  ss2iundf  44658  pm11.57  45372  pm11.59  45374  tratrb  45518  hbexg  45538  e2ebindALT  45910  modelaxreplem2  45968  permaxrep  45995  dvnmul  46952  stoweidlem34  47043  sge0fodjrnlem  47425  pimrecltpos  47717  pimrecltneg  47733  smfaddlem1  47772  smfresal  47797  smfinflem  47826  ichnfim  48545  ovmpordxf  49450