Theorem alrimi 2214

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

Syntax hints:   → wi 4  ∀wal 1535  Ⅎwnf 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-ex 1778  df-nf 1782

This theorem is referenced by:  sbalex  2243  sbimd  2246  sbbid  2247  nf5d  2288  axc4i  2326  19.12  2331  nfsbd  2530  mobid  2553  mo3  2567  eubid  2590  2moexv  2630  eupicka  2637  2moex  2643  2mo  2651  abbid  2813  nfcd  2901  nfabdwOLD  2933  ceqsalgALT  3526  ceqsexOLD  3541  vtocldf  3572  rspcdf  3622  elrab3t  3707  morex  3741  sbciedf  3849  csbiebt  3951  csbiedf  3952  ssrd  4013  eqrd  4028  invdisj  5152  zfrepclf  5312  eusv2nf  5413  ssopab2bw  5566  ssopab2b  5568  imadif  6662  eusvobj1  7441  ssoprab2b  7519  eqoprab2bw  7520  ovmpodxf  7600  axrepnd  10663  axunnd  10665  axpownd  10670  axregndlem1  10671  axacndlem1  10676  axacndlem2  10677  axacndlem3  10678  axacndlem4  10679  axacndlem5  10680  axacnd  10681  mreexexd  17706  acsmapd  18624  isch3  31273  ssrelf  32637  eqrelrd2  32638  esumeq12dvaf  33995  bnj1366  34805  bnj571  34882  bnj964  34919  iota5f  35686  bj-hbext  36676  bj-nfext  36678  wl-mo3t  37530  wl-ax11-lem3  37541  cover2  37675  alrimii  38079  mpobi123f  38122  mptbi12f  38126  ss2iundf  43621  pm11.57  44358  pm11.59  44360  tratrb  44507  hbexg  44527  e2ebindALT  44900  mpteq1dfOLD  45144  mpteq12daOLD  45151  dvnmul  45864  stoweidlem34  45955  sge0fodjrnlem  46337  pimrecltpos  46629  pimrecltneg  46645  smfaddlem1  46684  smfresal  46709  smfinflem  46738  smfinfmpt  46740  ichnfim  47338  ovmpordxf  48063  setrec1lem4  48782