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  4126  el  4223  exmid1dc  4245  exmidn0m  4246  exmid0el  4249  exmidundif  4251  exmidundifim  4252  exmid1stab  4253  euotd  4300  reusv1  4506  elirr  4590  sucprcreg  4598  en2lp  4603  tfisi  4636  ssrelrel  4776  issref  5066  iotaval  5244  iota5  5254  iotabidv  5255  funmo  5287  funco  5312  funun  5316  fununfun  5318  fununi  5343  funcnvuni  5344  funimaexglem  5358  fvssunirng  5593  relfvssunirn  5594  sefvex  5599  nfunsn  5613  f1oresrab  5747  funoprabg  6046  uchoice  6225  mpofvex  6293  1stconst  6309  2ndconst  6310  disjxp1  6324  tfrexlem  6422  tfr1onlemsucfn  6428  tfr1onlemsucaccv  6429  tfr1onlembxssdm  6431  tfr1onlembfn  6432  tfr1onlemaccex  6436  tfr1onlemres  6437  tfrcllemsucfn  6441  tfrcllemsucaccv  6442  tfrcllembxssdm  6444  tfrcllembfn  6445  tfrcllemaccex  6449  tfrcllemres  6450  tfrcl  6452  rdgexggg  6465  rdgifnon  6467  rdgifnon2  6468  rdgivallem  6469  frecabcl  6487  frectfr  6488  frecrdg  6496  iserd  6648  exmidpw  7007  exmidpweq  7008  exmidpw2en  7011  fiintim  7030  fisseneq  7033  sbthlemi3  7063  finomni  7244  exmidomniim  7245  exmidomni  7246  exmidfodomrlemr  7312  exmidfodomrlemrALT  7313  exmidmotap  7375  cc1  7379  pitonn  7963  frecuzrdgtcl  10559  frecuzrdgfunlem  10566  zfz1iso  10988  shftfn  11168  exmidunben  12830  prdsex  13134  imasex  13170  imasaddfnlemg  13179  lssex  14149  tgcl  14569  epttop  14595  neissex  14670  uptx  14779  dvfgg  15193  2spim  15739  decidr  15769  bj-om  15910  bj-nnord  15931  bj-inf2vn  15947  bj-inf2vn2  15948  bj-findis  15952  exmidsbthrlem  15998  sbthom  16002