Theorem alrimi 2220

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

Syntax hints:   → wi 4  ∀wal 1539  Ⅎwnf 1784

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2184

This theorem depends on definitions:  df-bi 207  df-ex 1781  df-nf 1785

This theorem is referenced by:  sbalex  2249  sbimd  2252  sbbid  2253  nf5d  2290  axc4i  2327  19.12  2332  nfsbd  2526  mobid  2550  mo3  2564  eubid  2587  2moexv  2627  eupicka  2634  2moex  2640  2mo  2648  abbid  2804  nfcd  2891  ceqsalgALT  3477  vtocldf  3517  rspcdf  3563  elrab3t  3645  morex  3677  sbciedf  3783  csbiebt  3878  csbiedf  3879  ssrd  3938  eqrd  3953  invdisj  5084  zfrepclf  5236  eusv2nf  5340  ssopab2bw  5495  ssopab2b  5497  imadif  6576  eusvobj1  7351  ssoprab2b  7427  eqoprab2bw  7428  ovmpodxf  7508  axrepnd  10507  axunnd  10509  axpownd  10514  axregndlem1  10515  axacndlem1  10520  axacndlem2  10521  axacndlem3  10522  axacndlem4  10523  axacndlem5  10524  axacnd  10525  mreexexd  17573  acsmapd  18479  isch3  31318  ssrelf  32695  eqrelrd2  32696  esumeq12dvaf  34190  bnj1366  34987  bnj571  35064  bnj964  35101  iota5f  35920  bj-hbext  36913  bj-nfext  36915  wl-mo3t  37783  cover2  37918  alrimii  38322  mpobi123f  38365  mptbi12f  38369  ss2iundf  43921  pm11.57  44651  pm11.59  44653  tratrb  44798  hbexg  44818  e2ebindALT  45190  modelaxreplem2  45241  permaxrep  45268  dvnmul  46208  stoweidlem34  46299  sge0fodjrnlem  46681  pimrecltpos  46973  pimrecltneg  46989  smfaddlem1  47028  smfresal  47053  smfinflem  47082  ichnfim  47731  ovmpordxf  48606  setrec1lem4  49956