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 1857	1 ⊢ (𝜑 → ∀𝑥𝜓)

This proof depends on syntax axioms:   → wi 4  ∀wal 1568  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2216

This proof depends on definitions:  df-bi 210  df-ex 1813  df-nf 1817

This theorem is used by:  sbalex  2281  sbimd  2283  sbbid  2284  nf5d  2321  axc4i  2357  19.12  2362  nfsbd  2556  mobid  2580  mo3  2594  eubid  2617  2moexv  2657  eupicka  2664  2moex  2670  2mo  2678  abbid  2833  nfcd  2920  ceqsalgALT  3493  vtocldf  3528  rspcdf  3570  elrab3t  3651  morex  3684  sbciedf  3788  csbiebt  3883  csbiedf  3884  ssrd  3943  eqrd  3957  invdisj  5097  zfrepclf  5254  eusv2nf  5368  ssopab2bw  5534  ssopab2b  5536  imadif  6624  eusvobj1  7412  ssoprab2b  7488  eqoprab2bw  7489  ovmpodxf  7569  axrepnd  10596  axunnd  10598  axpownd  10603  axregndlem1  10604  axacndlem1  10609  axacndlem2  10610  axacndlem3  10611  axacndlem4  10612  axacndlem5  10613  axacnd  10614  mreexexd  17728  acsmapd  18634  isch3  31666  ssrelf  33033  eqrelrd2  33034  esumeq12dvaf  34487  bnj1366  35284  bnj571  35361  bnj964  35398  iota5f  36255  axtcond  37048  bj-nfext  37398  wl-mo3t  38290  cover2  38426  alrimii  38828  mpobi123f  38871  mptbi12f  38875  ss2iundf  44445  pm11.57  45159  pm11.59  45161  tratrb  45305  hbexg  45325  e2ebindALT  45697  modelaxreplem2  45748  permaxrep  45775  dvnmul  46717  stoweidlem34  46808  sge0fodjrnlem  47190  pimrecltpos  47482  pimrecltneg  47498  smfaddlem1  47537  smfresal  47562  smfinflem  47591  ichnfim  48273  ovmpordxf  49178  setrec1lem4  50527