Theorem alrimiv 1897

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

Syntax hints:   → wi 4  ∀wal 1371

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1470  ax-gen 1472  ax-17 1549

This theorem is referenced by:  alrimivv  1898  nfdv  1900  sbbidv  1908  cbvalvw  1943  axext4  2189  eqrdv  2203  abbi2dv  2324  abbi1dv  2325  elex22  2787  elex2  2788  spcimdv  2857  spcimedv  2859  pm13.183  2911  sbcthdv  3013  sbcimdv  3064  ssrdv  3199  ss2abdv  3266  abssdv  3267  opprc  3840  dfnfc2  3868  intss  3906  intab  3914  dfiin2g  3960  disjss1  4027  mpteq12dva  4125  el  4222  exmid1dc  4244  exmidn0m  4245  exmid0el  4248  exmidundif  4250  exmidundifim  4251  exmid1stab  4252  euotd  4299  reusv1  4505  elirr  4589  sucprcreg  4597  en2lp  4602  tfisi  4635  ssrelrel  4775  issref  5065  iotaval  5243  iota5  5253  iotabidv  5254  funmo  5286  funco  5311  funun  5315  fununfun  5317  fununi  5342  funcnvuni  5343  funimaexglem  5357  fvssunirng  5591  relfvssunirn  5592  sefvex  5597  nfunsn  5611  f1oresrab  5745  funoprabg  6044  uchoice  6223  mpofvex  6291  1stconst  6307  2ndconst  6308  disjxp1  6322  tfrexlem  6420  tfr1onlemsucfn  6426  tfr1onlemsucaccv  6427  tfr1onlembxssdm  6429  tfr1onlembfn  6430  tfr1onlemaccex  6434  tfr1onlemres  6435  tfrcllemsucfn  6439  tfrcllemsucaccv  6440  tfrcllembxssdm  6442  tfrcllembfn  6443  tfrcllemaccex  6447  tfrcllemres  6448  tfrcl  6450  rdgexggg  6463  rdgifnon  6465  rdgifnon2  6466  rdgivallem  6467  frecabcl  6485  frectfr  6486  frecrdg  6494  iserd  6646  exmidpw  7005  exmidpweq  7006  exmidpw2en  7009  fiintim  7028  fisseneq  7031  sbthlemi3  7061  finomni  7242  exmidomniim  7243  exmidomni  7244  exmidfodomrlemr  7310  exmidfodomrlemrALT  7311  exmidmotap  7373  cc1  7377  pitonn  7961  frecuzrdgtcl  10557  frecuzrdgfunlem  10564  zfz1iso  10986  shftfn  11135  exmidunben  12797  prdsex  13101  imasex  13137  imasaddfnlemg  13146  lssex  14116  tgcl  14536  epttop  14562  neissex  14637  uptx  14746  dvfgg  15160  2spim  15702  decidr  15732  bj-om  15873  bj-nnord  15894  bj-inf2vn  15910  bj-inf2vn2  15911  bj-findis  15915  exmidsbthrlem  15961  sbthom  15965