Theorem alrimi 2221

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

Syntax hints:   → wi 4  ∀wal 1540  Ⅎwnf 1785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-ex 1782  df-nf 1786

This theorem is referenced by:  sbalex  2250  sbimd  2253  sbbid  2254  nf5d  2291  axc4i  2328  19.12  2333  nfsbd  2527  mobid  2551  mo3  2565  eubid  2588  2moexv  2628  eupicka  2635  2moex  2641  2mo  2649  abbid  2805  nfcd  2892  ceqsalgALT  3467  vtocldf  3506  rspcdf  3552  elrab3t  3634  morex  3666  sbciedf  3772  csbiebt  3867  csbiedf  3868  ssrd  3927  eqrd  3942  invdisj  5072  zfrepclf  5227  eusv2nf  5333  ssopab2bw  5496  ssopab2b  5498  imadif  6577  eusvobj1  7354  ssoprab2b  7430  eqoprab2bw  7431  ovmpodxf  7511  axrepnd  10511  axunnd  10513  axpownd  10518  axregndlem1  10519  axacndlem1  10524  axacndlem2  10525  axacndlem3  10526  axacndlem4  10527  axacndlem5  10528  axacnd  10529  mreexexd  17608  acsmapd  18514  isch3  31330  ssrelf  32706  eqrelrd2  32707  esumeq12dvaf  34194  bnj1366  34990  bnj571  35067  bnj964  35104  iota5f  35925  axtcond  36679  bj-nfext  37030  wl-mo3t  37918  cover2  38053  alrimii  38457  mpobi123f  38500  mptbi12f  38504  ss2iundf  44107  pm11.57  44837  pm11.59  44839  tratrb  44984  hbexg  45004  e2ebindALT  45376  modelaxreplem2  45427  permaxrep  45454  dvnmul  46392  stoweidlem34  46483  sge0fodjrnlem  46865  pimrecltpos  47157  pimrecltneg  47173  smfaddlem1  47212  smfresal  47237  smfinflem  47266  ichnfim  47939  ovmpordxf  48830  setrec1lem4  50180