Theorem alrimi 2199

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

Syntax hints:   → wi 4  ∀wal 1532  Ⅎwnf 1778

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-12 2164

This theorem depends on definitions:  df-bi 206  df-ex 1775  df-nf 1779

This theorem is referenced by:  sbimd  2230  sbbid  2231  nf5d  2273  axc4i  2310  19.12  2315  nfsbd  2516  mobid  2539  mo3  2553  eubid  2576  2moexv  2618  eupicka  2625  2moex  2631  2mo  2639  abbid  2798  nfcd  2886  nfabdwOLD  2922  ceqsalgALT  3504  ceqsexOLD  3520  vtocldf  3542  rspcdf  3594  elrab3t  3679  morex  3712  sbciedf  3818  csbiebt  3919  csbiedf  3920  ssrd  3983  eqrd  3997  invdisj  5126  zfrepclf  5288  eusv2nf  5389  ssopab2bw  5543  ssopab2b  5545  imadif  6631  eusvobj1  7407  ssoprab2b  7483  eqoprab2bw  7484  ovmpodxf  7565  axrepnd  10609  axunnd  10611  axpownd  10616  axregndlem1  10617  axacndlem1  10622  axacndlem2  10623  axacndlem3  10624  axacndlem4  10625  axacndlem5  10626  axacnd  10627  mreexexd  17619  acsmapd  18537  isch3  31038  ssrelf  32388  eqrelrd2  32389  esumeq12dvaf  33586  bnj1366  34396  bnj571  34473  bnj964  34510  iota5f  35254  bj-hbext  36123  bj-nfext  36125  wl-mo3t  36978  wl-ax11-lem3  36989  cover2  37123  alrimii  37527  mpobi123f  37570  mptbi12f  37574  ss2iundf  43012  pm11.57  43749  pm11.59  43751  tratrb  43898  hbexg  43918  e2ebindALT  44291  mpteq1dfOLD  44534  mpteq12daOLD  44541  dvnmul  45254  stoweidlem34  45345  sge0fodjrnlem  45727  pimrecltpos  46019  pimrecltneg  46035  smfaddlem1  46074  smfresal  46099  smfinflem  46128  smfinfmpt  46130  ichnfim  46727  ovmpordxf  47325  setrec1lem4  48044