Theorem alrimiv 1874

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 1526	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		alrimiv.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	alrimih 1469	1 ⊢ (𝜑 → ∀𝑥𝜓)

Syntax hints:   → wi 4  ∀wal 1351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1447  ax-gen 1449  ax-17 1526

This theorem is referenced by:  alrimivv  1875  nfdv  1877  cbvalvw  1919  axext4  2161  eqrdv  2175  abbi2dv  2296  abbi1dv  2297  elex22  2754  elex2  2755  spcimdv  2823  spcimedv  2825  pm13.183  2877  sbcthdv  2979  sbcimdv  3030  ssrdv  3163  ss2abdv  3230  abssdv  3231  opprc  3801  dfnfc2  3829  intss  3867  intab  3875  dfiin2g  3921  disjss1  3988  mpteq12dva  4086  el  4180  exmid1dc  4202  exmidn0m  4203  exmid0el  4206  exmidundif  4208  exmidundifim  4209  exmid1stab  4210  euotd  4256  reusv1  4460  elirr  4542  sucprcreg  4550  en2lp  4555  tfisi  4588  ssrelrel  4728  issref  5013  iotaval  5191  iota5  5200  iotabidv  5201  funmo  5233  funco  5258  funun  5262  fununi  5286  funcnvuni  5287  funimaexglem  5301  fvssunirng  5532  relfvssunirn  5533  sefvex  5538  nfunsn  5551  f1oresrab  5683  funoprabg  5976  mpofvex  6206  1stconst  6224  2ndconst  6225  disjxp1  6239  tfrexlem  6337  tfr1onlemsucfn  6343  tfr1onlemsucaccv  6344  tfr1onlembxssdm  6346  tfr1onlembfn  6347  tfr1onlemaccex  6351  tfr1onlemres  6352  tfrcllemsucfn  6356  tfrcllemsucaccv  6357  tfrcllembxssdm  6359  tfrcllembfn  6360  tfrcllemaccex  6364  tfrcllemres  6365  tfrcl  6367  rdgexggg  6380  rdgifnon  6382  rdgifnon2  6383  rdgivallem  6384  frecabcl  6402  frectfr  6403  frecrdg  6411  iserd  6563  exmidpw  6910  exmidpweq  6911  fiintim  6930  fisseneq  6933  sbthlemi3  6960  finomni  7140  exmidomniim  7141  exmidomni  7142  exmidfodomrlemr  7203  exmidfodomrlemrALT  7204  exmidmotap  7262  cc1  7266  pitonn  7849  frecuzrdgtcl  10414  frecuzrdgfunlem  10421  zfz1iso  10823  shftfn  10835  exmidunben  12429  prdsex  12723  imasex  12731  imasaddfnlemg  12740  tgcl  13603  epttop  13629  neissex  13704  uptx  13813  dvfgg  14196  2spim  14557  decidr  14587  bj-om  14728  bj-nnord  14749  bj-inf2vn  14765  bj-inf2vn2  14766  bj-findis  14770  exmidsbthrlem  14809  sbthom  14813