Theorem alrimi 2216

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

Syntax hints:   → wi 4  ∀wal 1539  Ⅎwnf 1784

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2180

This theorem depends on definitions:  df-bi 207  df-ex 1781  df-nf 1785

This theorem is referenced by:  sbalex  2245  sbimd  2248  sbbid  2249  nf5d  2286  axc4i  2323  19.12  2328  nfsbd  2522  mobid  2545  mo3  2559  eubid  2582  2moexv  2622  eupicka  2629  2moex  2635  2mo  2643  abbid  2799  nfcd  2887  ceqsalgALT  3473  vtocldf  3513  rspcdf  3559  elrab3t  3641  morex  3673  sbciedf  3779  csbiebt  3874  csbiedf  3875  ssrd  3934  eqrd  3949  invdisj  5075  zfrepclf  5227  eusv2nf  5331  ssopab2bw  5485  ssopab2b  5487  imadif  6565  eusvobj1  7339  ssoprab2b  7415  eqoprab2bw  7416  ovmpodxf  7496  axrepnd  10485  axunnd  10487  axpownd  10492  axregndlem1  10493  axacndlem1  10498  axacndlem2  10499  axacndlem3  10500  axacndlem4  10501  axacndlem5  10502  axacnd  10503  mreexexd  17554  acsmapd  18460  isch3  31221  ssrelf  32598  eqrelrd2  32599  esumeq12dvaf  34044  bnj1366  34841  bnj571  34918  bnj964  34955  iota5f  35768  bj-hbext  36754  bj-nfext  36756  wl-mo3t  37620  wl-ax11-lem3  37631  cover2  37765  alrimii  38169  mpobi123f  38212  mptbi12f  38216  ss2iundf  43762  pm11.57  44492  pm11.59  44494  tratrb  44639  hbexg  44659  e2ebindALT  45031  modelaxreplem2  45082  permaxrep  45109  dvnmul  46051  stoweidlem34  46142  sge0fodjrnlem  46524  pimrecltpos  46816  pimrecltneg  46832  smfaddlem1  46871  smfresal  46896  smfinflem  46925  ichnfim  47574  ovmpordxf  48449  setrec1lem4  49801