Theorem alrimiv 1888

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

Syntax hints:   → wi 4  ∀wal 1362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1461  ax-gen 1463  ax-17 1540

This theorem is referenced by:  alrimivv  1889  nfdv  1891  sbbidv  1899  cbvalvw  1934  axext4  2180  eqrdv  2194  abbi2dv  2315  abbi1dv  2316  elex22  2778  elex2  2779  spcimdv  2848  spcimedv  2850  pm13.183  2902  sbcthdv  3004  sbcimdv  3055  ssrdv  3189  ss2abdv  3256  abssdv  3257  opprc  3829  dfnfc2  3857  intss  3895  intab  3903  dfiin2g  3949  disjss1  4016  mpteq12dva  4114  el  4211  exmid1dc  4233  exmidn0m  4234  exmid0el  4237  exmidundif  4239  exmidundifim  4240  exmid1stab  4241  euotd  4287  reusv1  4493  elirr  4577  sucprcreg  4585  en2lp  4590  tfisi  4623  ssrelrel  4763  issref  5052  iotaval  5230  iota5  5240  iotabidv  5241  funmo  5273  funco  5298  funun  5302  fununi  5326  funcnvuni  5327  funimaexglem  5341  fvssunirng  5573  relfvssunirn  5574  sefvex  5579  nfunsn  5593  f1oresrab  5727  funoprabg  6021  uchoice  6195  mpofvex  6263  1stconst  6279  2ndconst  6280  disjxp1  6294  tfrexlem  6392  tfr1onlemsucfn  6398  tfr1onlemsucaccv  6399  tfr1onlembxssdm  6401  tfr1onlembfn  6402  tfr1onlemaccex  6406  tfr1onlemres  6407  tfrcllemsucfn  6411  tfrcllemsucaccv  6412  tfrcllembxssdm  6414  tfrcllembfn  6415  tfrcllemaccex  6419  tfrcllemres  6420  tfrcl  6422  rdgexggg  6435  rdgifnon  6437  rdgifnon2  6438  rdgivallem  6439  frecabcl  6457  frectfr  6458  frecrdg  6466  iserd  6618  exmidpw  6969  exmidpweq  6970  exmidpw2en  6973  fiintim  6992  fisseneq  6995  sbthlemi3  7025  finomni  7206  exmidomniim  7207  exmidomni  7208  exmidfodomrlemr  7269  exmidfodomrlemrALT  7270  exmidmotap  7328  cc1  7332  pitonn  7915  frecuzrdgtcl  10504  frecuzrdgfunlem  10511  zfz1iso  10933  shftfn  10989  exmidunben  12643  prdsex  12940  imasex  12948  imasaddfnlemg  12957  lssex  13910  tgcl  14300  epttop  14326  neissex  14401  uptx  14510  dvfgg  14924  2spim  15412  decidr  15442  bj-om  15583  bj-nnord  15604  bj-inf2vn  15620  bj-inf2vn2  15621  bj-findis  15625  exmidsbthrlem  15666  sbthom  15670