Theorem alrimi 2218

Description: Inference form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2212. (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 2200	. 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 2182

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

This theorem is referenced by:  sbalex  2247  sbimd  2250  sbbid  2251  nf5d  2288  axc4i  2325  19.12  2330  nfsbd  2524  mobid  2548  mo3  2562  eubid  2585  2moexv  2625  eupicka  2632  2moex  2638  2mo  2646  abbid  2802  nfcd  2889  ceqsalgALT  3475  vtocldf  3515  rspcdf  3561  elrab3t  3643  morex  3675  sbciedf  3781  csbiebt  3876  csbiedf  3877  ssrd  3936  eqrd  3951  invdisj  5082  zfrepclf  5234  eusv2nf  5338  ssopab2bw  5493  ssopab2b  5495  imadif  6574  eusvobj1  7349  ssoprab2b  7425  eqoprab2bw  7426  ovmpodxf  7506  axrepnd  10503  axunnd  10505  axpownd  10510  axregndlem1  10511  axacndlem1  10516  axacndlem2  10517  axacndlem3  10518  axacndlem4  10519  axacndlem5  10520  axacnd  10521  mreexexd  17569  acsmapd  18475  isch3  31265  ssrelf  32642  eqrelrd2  32643  esumeq12dvaf  34137  bnj1366  34934  bnj571  35011  bnj964  35048  iota5f  35867  bj-hbext  36854  bj-nfext  36856  wl-mo3t  37720  cover2  37855  alrimii  38259  mpobi123f  38302  mptbi12f  38306  ss2iundf  43842  pm11.57  44572  pm11.59  44574  tratrb  44719  hbexg  44739  e2ebindALT  45111  modelaxreplem2  45162  permaxrep  45189  dvnmul  46129  stoweidlem34  46220  sge0fodjrnlem  46602  pimrecltpos  46894  pimrecltneg  46910  smfaddlem1  46949  smfresal  46974  smfinflem  47003  ichnfim  47652  ovmpordxf  48527  setrec1lem4  49877