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  5226  eusv2nf  5332  ssopab2bw  5495  ssopab2b  5497  imadif  6576  eusvobj1  7353  ssoprab2b  7429  eqoprab2bw  7430  ovmpodxf  7510  axrepnd  10508  axunnd  10510  axpownd  10515  axregndlem1  10516  axacndlem1  10521  axacndlem2  10522  axacndlem3  10523  axacndlem4  10524  axacndlem5  10525  axacnd  10526  mreexexd  17605  acsmapd  18511  isch3  31327  ssrelf  32703  eqrelrd2  32704  esumeq12dvaf  34191  bnj1366  34987  bnj571  35064  bnj964  35101  iota5f  35922  axtcond  36676  bj-nfext  37027  wl-mo3t  37915  cover2  38050  alrimii  38454  mpobi123f  38497  mptbi12f  38501  ss2iundf  44104  pm11.57  44834  pm11.59  44836  tratrb  44981  hbexg  45001  e2ebindALT  45373  modelaxreplem2  45424  permaxrep  45451  dvnmul  46389  stoweidlem34  46480  sge0fodjrnlem  46862  pimrecltpos  47154  pimrecltneg  47170  smfaddlem1  47209  smfresal  47234  smfinflem  47263  ichnfim  47936  ovmpordxf  48827  setrec1lem4  50177