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  2752  elex2  2753  spcimdv  2821  spcimedv  2823  pm13.183  2875  sbcthdv  2977  sbcimdv  3028  ssrdv  3161  ss2abdv  3228  abssdv  3229  opprc  3798  dfnfc2  3826  intss  3864  intab  3872  dfiin2g  3918  disjss1  3984  mpteq12dva  4082  el  4176  exmid1dc  4198  exmidn0m  4199  exmid0el  4202  exmidundif  4204  exmidundifim  4205  exmid1stab  4206  euotd  4252  reusv1  4456  elirr  4538  sucprcreg  4546  en2lp  4551  tfisi  4584  ssrelrel  4724  issref  5008  iotaval  5186  iota5  5195  iotabidv  5196  funmo  5228  funco  5253  funun  5257  fununi  5281  funcnvuni  5282  funimaexglem  5296  fvssunirng  5527  relfvssunirn  5528  sefvex  5533  nfunsn  5546  f1oresrab  5678  funoprabg  5969  mpofvex  6199  1stconst  6217  2ndconst  6218  disjxp1  6232  tfrexlem  6330  tfr1onlemsucfn  6336  tfr1onlemsucaccv  6337  tfr1onlembxssdm  6339  tfr1onlembfn  6340  tfr1onlemaccex  6344  tfr1onlemres  6345  tfrcllemsucfn  6349  tfrcllemsucaccv  6350  tfrcllembxssdm  6352  tfrcllembfn  6353  tfrcllemaccex  6357  tfrcllemres  6358  tfrcl  6360  rdgexggg  6373  rdgifnon  6375  rdgifnon2  6376  rdgivallem  6377  frecabcl  6395  frectfr  6396  frecrdg  6404  iserd  6556  exmidpw  6903  exmidpweq  6904  fiintim  6923  fisseneq  6926  sbthlemi3  6953  finomni  7133  exmidomniim  7134  exmidomni  7135  exmidfodomrlemr  7196  exmidfodomrlemrALT  7197  exmidmotap  7255  cc1  7259  pitonn  7842  frecuzrdgtcl  10405  frecuzrdgfunlem  10412  zfz1iso  10812  shftfn  10824  exmidunben  12417  tgcl  13346  epttop  13372  neissex  13447  uptx  13556  dvfgg  13939  2spim  14289  decidr  14319  bj-om  14460  bj-nnord  14481  bj-inf2vn  14497  bj-inf2vn2  14498  bj-findis  14502  exmidsbthrlem  14541  sbthom  14545