Theorem alrimi 2214

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

Syntax hints:   → wi 4  ∀wal 1538  Ⅎwnf 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784

This theorem is referenced by:  sbalex  2243  sbimd  2246  sbbid  2247  nf5d  2284  axc4i  2321  19.12  2326  nfsbd  2520  mobid  2543  mo3  2557  eubid  2580  2moexv  2620  eupicka  2627  2moex  2633  2mo  2641  abbid  2797  nfcd  2884  ceqsalgALT  3481  ceqsexOLD  3494  vtocldf  3523  rspcdf  3572  elrab3t  3655  morex  3687  sbciedf  3793  csbiebt  3888  csbiedf  3889  ssrd  3948  eqrd  3963  invdisj  5088  zfrepclf  5241  eusv2nf  5345  ssopab2bw  5502  ssopab2b  5504  imadif  6584  eusvobj1  7362  ssoprab2b  7438  eqoprab2bw  7439  ovmpodxf  7519  axrepnd  10523  axunnd  10525  axpownd  10530  axregndlem1  10531  axacndlem1  10536  axacndlem2  10537  axacndlem3  10538  axacndlem4  10539  axacndlem5  10540  axacnd  10541  mreexexd  17589  acsmapd  18495  isch3  31220  ssrelf  32593  eqrelrd2  32594  esumeq12dvaf  34014  bnj1366  34812  bnj571  34889  bnj964  34926  iota5f  35704  bj-hbext  36691  bj-nfext  36693  wl-mo3t  37557  wl-ax11-lem3  37568  cover2  37702  alrimii  38106  mpobi123f  38149  mptbi12f  38153  ss2iundf  43641  pm11.57  44371  pm11.59  44373  tratrb  44519  hbexg  44539  e2ebindALT  44911  modelaxreplem2  44962  permaxrep  44989  dvnmul  45934  stoweidlem34  46025  sge0fodjrnlem  46407  pimrecltpos  46699  pimrecltneg  46715  smfaddlem1  46754  smfresal  46779  smfinflem  46808  ichnfim  47458  ovmpordxf  48320  setrec1lem4  49672