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  3484  ceqsexOLD  3497  vtocldf  3526  rspcdf  3575  elrab3t  3658  morex  3690  sbciedf  3796  csbiebt  3891  csbiedf  3892  ssrd  3951  eqrd  3966  invdisj  5093  zfrepclf  5246  eusv2nf  5350  ssopab2bw  5507  ssopab2b  5509  imadif  6600  eusvobj1  7380  ssoprab2b  7458  eqoprab2bw  7459  ovmpodxf  7539  axrepnd  10547  axunnd  10549  axpownd  10554  axregndlem1  10555  axacndlem1  10560  axacndlem2  10561  axacndlem3  10562  axacndlem4  10563  axacndlem5  10564  axacnd  10565  mreexexd  17609  acsmapd  18513  isch3  31170  ssrelf  32543  eqrelrd2  32544  esumeq12dvaf  34021  bnj1366  34819  bnj571  34896  bnj964  34933  iota5f  35711  bj-hbext  36698  bj-nfext  36700  wl-mo3t  37564  wl-ax11-lem3  37575  cover2  37709  alrimii  38113  mpobi123f  38156  mptbi12f  38160  ss2iundf  43648  pm11.57  44378  pm11.59  44380  tratrb  44526  hbexg  44546  e2ebindALT  44918  modelaxreplem2  44969  permaxrep  44996  dvnmul  45941  stoweidlem34  46032  sge0fodjrnlem  46414  pimrecltpos  46706  pimrecltneg  46722  smfaddlem1  46761  smfresal  46786  smfinflem  46815  ichnfim  47465  ovmpordxf  48327  setrec1lem4  49679