Theorem alrimi 2252

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1567  Ⅎwnf 1815

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-12 2215

This proof depends on definitions:  df-bi 210  df-ex 1812  df-nf 1816

This theorem is used by:  sbalex  2281  sbimd  2283  sbbid  2284  nf5d  2320  axc4i  2355  19.12  2360  nfsbd  2554  mobid  2578  mo3  2592  eubid  2615  2moexv  2655  eupicka  2662  2moex  2668  2mo  2676  abbid  2831  nfcd  2919  ceqsalgALT  3490  vtocldf  3525  rspcdf  3567  elrab3t  3647  morex  3680  sbciedf  3784  csbiebt  3880  csbiedf  3881  ssrd  3918  eqrd  3932  invdisj  5092  zfrepclf  5247  eusv2nf  5361  ssopab2bw  5526  ssopab2b  5528  imadif  6635  eusvobj1  7423  ssoprab2b  7499  eqoprab2bw  7500  ovmpodxf  7580  setrec1lem4  9984  axrepnd  10692  axunnd  10694  axpownd  10699  axregndlem1  10700  axacndlem1  10705  axacndlem2  10706  axacndlem3  10707  axacndlem4  10708  axacndlem5  10709  axacnd  10710  mreexexd  17837  acsmapd  18743  isch3  31858  ssrelf  33266  eqrelrd2  33267  esumeq12dvaf  34719  bnj1366  35515  bnj571  35592  bnj964  35629  srepdflem2  36043  srepdf  36044  iota5f  36619  axtcond  37396  bj-nfext  37746  wl-mo3t  38651  cover2  38792  alrimii  39194  mpobi123f  39237  mptbi12f  39241  ss2iundf  44802  pm11.57  45516  pm11.59  45518  tratrb  45661  hbexg  45681  e2ebindALT  46053  modelaxreplem2  46111  permaxrep  46138  dvnmul  47095  stoweidlem34  47186  sge0fodjrnlem  47568  pimrecltpos  47860  pimrecltneg  47876  smfaddlem1  47915  smfresal  47940  smfinflem  47969  ichnfim  48688  ovmpordxf  49593