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  2327  19.12  2332  nfsbd  2526  mobid  2550  mo3  2564  eubid  2587  2moexv  2627  eupicka  2634  2moex  2640  2mo  2648  abbid  2804  nfcd  2891  ceqsalgALT  3466  vtocldf  3505  rspcdf  3551  elrab3t  3633  morex  3665  sbciedf  3771  csbiebt  3866  csbiedf  3867  ssrd  3926  eqrd  3941  invdisj  5071  zfrepclf  5226  eusv2nf  5337  ssopab2bw  5502  ssopab2b  5504  imadif  6582  eusvobj1  7360  ssoprab2b  7436  eqoprab2bw  7437  ovmpodxf  7517  axrepnd  10517  axunnd  10519  axpownd  10524  axregndlem1  10525  axacndlem1  10530  axacndlem2  10531  axacndlem3  10532  axacndlem4  10533  axacndlem5  10534  axacnd  10535  mreexexd  17614  acsmapd  18520  isch3  31312  ssrelf  32688  eqrelrd2  32689  esumeq12dvaf  34175  bnj1366  34971  bnj571  35048  bnj964  35085  iota5f  35906  axtcond  36660  bj-nfext  37011  wl-mo3t  37901  cover2  38036  alrimii  38440  mpobi123f  38483  mptbi12f  38487  ss2iundf  44086  pm11.57  44816  pm11.59  44818  tratrb  44963  hbexg  44983  e2ebindALT  45355  modelaxreplem2  45406  permaxrep  45433  dvnmul  46371  stoweidlem34  46462  sge0fodjrnlem  46844  pimrecltpos  47136  pimrecltneg  47152  smfaddlem1  47191  smfresal  47216  smfinflem  47245  ichnfim  47924  ovmpordxf  48815  setrec1lem4  50165