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  3479  vtocldf  3519  rspcdf  3565  elrab3t  3647  morex  3679  sbciedf  3785  csbiebt  3880  csbiedf  3881  ssrd  3940  eqrd  3955  invdisj  5086  zfrepclf  5238  eusv2nf  5342  ssopab2bw  5503  ssopab2b  5505  imadif  6584  eusvobj1  7361  ssoprab2b  7437  eqoprab2bw  7438  ovmpodxf  7518  axrepnd  10517  axunnd  10519  axpownd  10524  axregndlem1  10525  axacndlem1  10530  axacndlem2  10531  axacndlem3  10532  axacndlem4  10533  axacndlem5  10534  axacnd  10535  mreexexd  17583  acsmapd  18489  isch3  31333  ssrelf  32709  eqrelrd2  32710  esumeq12dvaf  34213  bnj1366  35009  bnj571  35086  bnj964  35123  iota5f  35944  bj-hbext  36959  bj-nfext  36961  wl-mo3t  37835  cover2  37970  alrimii  38374  mpobi123f  38417  mptbi12f  38421  ss2iundf  44019  pm11.57  44749  pm11.59  44751  tratrb  44896  hbexg  44916  e2ebindALT  45288  modelaxreplem2  45339  permaxrep  45366  dvnmul  46305  stoweidlem34  46396  sge0fodjrnlem  46778  pimrecltpos  47070  pimrecltneg  47086  smfaddlem1  47125  smfresal  47150  smfinflem  47179  ichnfim  47828  ovmpordxf  48703  setrec1lem4  50053