Theorem alrimiv 1922

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
alrimiv.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
alrimiv	⊢ (𝜑 → ∀𝑥𝜓)

Distinct variable group:   𝜑,𝑥

Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem alrimiv

Step	Hyp	Ref	Expression
1		ax-17 1575	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		alrimiv.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	alrimih 1518	1 ⊢ (𝜑 → ∀𝑥𝜓)

Syntax hints:   → wi 4  ∀wal 1396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1496  ax-gen 1498  ax-17 1575

This theorem is referenced by:  alrimivv  1923  nfdv  1925  sbbidv  1933  cbvalvw  1968  axext4  2215  eqrdv  2229  abbi2dv  2351  abbi1dv  2352  elex22  2819  elex2  2820  spcimdv  2891  spcimedv  2893  pm13.183  2945  sbcthdv  3047  sbcimdv  3098  ssrdv  3234  ss2abdv  3301  abssdv  3302  opprc  3888  dfnfc2  3916  intss  3954  intab  3962  dfiin2g  4008  disjss1  4075  mpteq12dva  4175  el  4274  exmid1dc  4296  exmidn0m  4297  exmid0el  4300  exmidundif  4302  exmidundifim  4303  exmid1stab  4304  euotd  4353  reusv1  4561  elirr  4645  sucprcreg  4653  en2lp  4658  tfisi  4691  ssrelrel  4832  issref  5126  iotaval  5305  iota5  5315  iotabidv  5316  funmo  5348  funco  5373  funun  5378  fununfun  5380  fununi  5405  funcnvuni  5406  funimaexglem  5420  fvssunirng  5663  relfvssunirn  5664  sefvex  5669  nfunsn  5685  f1oresrab  5820  funoprabg  6130  uchoice  6309  mpofvex  6379  1stconst  6395  2ndconst  6396  disjxp1  6410  tfrexlem  6543  tfr1onlemsucfn  6549  tfr1onlemsucaccv  6550  tfr1onlembxssdm  6552  tfr1onlembfn  6553  tfr1onlemaccex  6557  tfr1onlemres  6558  tfrcllemsucfn  6562  tfrcllemsucaccv  6563  tfrcllembxssdm  6565  tfrcllembfn  6566  tfrcllemaccex  6570  tfrcllemres  6571  tfrcl  6573  rdgexggg  6586  rdgifnon  6588  rdgifnon2  6589  rdgivallem  6590  frecabcl  6608  frectfr  6609  frecrdg  6617  iserd  6771  modom  7037  exmidpw  7143  exmidpweq  7144  exmidpw2en  7147  fiintim  7166  fisseneq  7170  sbthlemi3  7201  finomni  7399  exmidomniim  7400  exmidomni  7401  exmidfodomrlemr  7473  exmidfodomrlemrALT  7474  exmidmotap  7540  cc1  7544  pitonn  8128  frecuzrdgtcl  10737  frecuzrdgfunlem  10744  zfz1iso  11168  shftfn  11464  exmidunben  13127  prdsex  13432  imasex  13468  imasaddfnlemg  13477  lssex  14450  tgcl  14875  epttop  14901  neissex  14976  uptx  15085  dvfgg  15499  upgrspanop  16224  umgrspanop  16225  usgrspanop  16226  2spim  16484  decidr  16514  bj-om  16653  bj-nnord  16674  bj-inf2vn  16690  bj-inf2vn2  16691  bj-findis  16695  exmidsbthrlem  16750  sbthom  16754