Theorem alrimi 2249

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

Syntax hints:   → wi 4  ∀wal 1568  Ⅎwnf 1813

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-12 2213

This theorem depends on definitions:  df-bi 210  df-ex 1810  df-nf 1814

This theorem is referenced by:  sbalex  2278  sbimd  2281  sbbid  2282  nf5d  2319  axc4i  2355  19.12  2360  nfsbd  2554  mobid  2578  mo3  2592  eubid  2615  2moexv  2655  eupicka  2662  2moex  2668  2mo  2676  abbid  2831  nfcd  2918  ceqsalgALT  3491  vtocldf  3526  rspcdf  3568  elrab3t  3649  morex  3682  sbciedf  3786  csbiebt  3882  csbiedf  3883  ssrd  3942  eqrd  3956  invdisj  5095  zfrepclf  5252  eusv2nf  5366  ssopab2bw  5532  ssopab2b  5534  imadif  6620  eusvobj1  7403  ssoprab2b  7479  eqoprab2bw  7480  ovmpodxf  7560  axrepnd  10574  axunnd  10576  axpownd  10581  axregndlem1  10582  axacndlem1  10587  axacndlem2  10588  axacndlem3  10589  axacndlem4  10590  axacndlem5  10591  axacnd  10592  mreexexd  17699  acsmapd  18605  isch3  31593  ssrelf  32960  eqrelrd2  32961  esumeq12dvaf  34421  bnj1366  35217  bnj571  35294  bnj964  35331  iota5f  36216  axtcond  37009  bj-nfext  37359  wl-mo3t  38251  cover2  38386  alrimii  38788  mpobi123f  38831  mptbi12f  38835  ss2iundf  44405  pm11.57  45119  pm11.59  45121  tratrb  45265  hbexg  45285  e2ebindALT  45657  modelaxreplem2  45708  permaxrep  45735  dvnmul  46677  stoweidlem34  46768  sge0fodjrnlem  47150  pimrecltpos  47442  pimrecltneg  47458  smfaddlem1  47497  smfresal  47522  smfinflem  47551  ichnfim  48233  ovmpordxf  49139  setrec1lem4  50488