Theorem alrimi 2212

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

Syntax hints:   → wi 4  ∀wal 1537  Ⅎwnf 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-12 2176

This theorem depends on definitions:  df-bi 207  df-ex 1779  df-nf 1783

This theorem is referenced by:  sbalex  2241  sbimd  2244  sbbid  2245  nf5d  2283  axc4i  2321  19.12  2326  nfsbd  2525  mobid  2548  mo3  2562  eubid  2585  2moexv  2625  eupicka  2632  2moex  2638  2mo  2646  abbid  2802  nfcd  2890  ceqsalgALT  3495  ceqsexOLD  3508  vtocldf  3537  rspcdf  3586  elrab3t  3668  morex  3700  sbciedf  3806  csbiebt  3901  csbiedf  3902  ssrd  3961  eqrd  3976  invdisj  5102  zfrepclf  5258  eusv2nf  5362  ssopab2bw  5519  ssopab2b  5521  imadif  6616  eusvobj1  7392  ssoprab2b  7470  eqoprab2bw  7471  ovmpodxf  7551  axrepnd  10600  axunnd  10602  axpownd  10607  axregndlem1  10608  axacndlem1  10613  axacndlem2  10614  axacndlem3  10615  axacndlem4  10616  axacndlem5  10617  axacnd  10618  mreexexd  17645  acsmapd  18549  isch3  31154  ssrelf  32528  eqrelrd2  32529  esumeq12dvaf  33970  bnj1366  34781  bnj571  34858  bnj964  34895  iota5f  35662  bj-hbext  36649  bj-nfext  36651  wl-mo3t  37515  wl-ax11-lem3  37526  cover2  37660  alrimii  38064  mpobi123f  38107  mptbi12f  38111  ss2iundf  43608  pm11.57  44339  pm11.59  44341  tratrb  44487  hbexg  44507  e2ebindALT  44880  modelaxreplem2  44931  permaxrep  44958  dvnmul  45902  stoweidlem34  45993  sge0fodjrnlem  46375  pimrecltpos  46667  pimrecltneg  46683  smfaddlem1  46722  smfresal  46747  smfinflem  46776  ichnfim  47396  ovmpordxf  48200  setrec1lem4  49274