Theorem alrimiv 1898

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

Syntax hints:   → wi 4  ∀wal 1371

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1471  ax-gen 1473  ax-17 1550

This theorem is referenced by:  alrimivv  1899  nfdv  1901  sbbidv  1909  cbvalvw  1944  axext4  2191  eqrdv  2205  abbi2dv  2326  abbi1dv  2327  elex22  2792  elex2  2793  spcimdv  2864  spcimedv  2866  pm13.183  2918  sbcthdv  3020  sbcimdv  3071  ssrdv  3207  ss2abdv  3274  abssdv  3275  opprc  3854  dfnfc2  3882  intss  3920  intab  3928  dfiin2g  3974  disjss1  4041  mpteq12dva  4141  el  4238  exmid1dc  4260  exmidn0m  4261  exmid0el  4264  exmidundif  4266  exmidundifim  4267  exmid1stab  4268  euotd  4317  reusv1  4523  elirr  4607  sucprcreg  4615  en2lp  4620  tfisi  4653  ssrelrel  4793  issref  5084  iotaval  5262  iota5  5272  iotabidv  5273  funmo  5305  funco  5330  funun  5334  fununfun  5336  fununi  5361  funcnvuni  5362  funimaexglem  5376  fvssunirng  5614  relfvssunirn  5615  sefvex  5620  nfunsn  5634  f1oresrab  5768  funoprabg  6067  uchoice  6246  mpofvex  6314  1stconst  6330  2ndconst  6331  disjxp1  6345  tfrexlem  6443  tfr1onlemsucfn  6449  tfr1onlemsucaccv  6450  tfr1onlembxssdm  6452  tfr1onlembfn  6453  tfr1onlemaccex  6457  tfr1onlemres  6458  tfrcllemsucfn  6462  tfrcllemsucaccv  6463  tfrcllembxssdm  6465  tfrcllembfn  6466  tfrcllemaccex  6470  tfrcllemres  6471  tfrcl  6473  rdgexggg  6486  rdgifnon  6488  rdgifnon2  6489  rdgivallem  6490  frecabcl  6508  frectfr  6509  frecrdg  6517  iserd  6669  exmidpw  7031  exmidpweq  7032  exmidpw2en  7035  fiintim  7054  fisseneq  7057  sbthlemi3  7087  finomni  7268  exmidomniim  7269  exmidomni  7270  exmidfodomrlemr  7341  exmidfodomrlemrALT  7342  exmidmotap  7408  cc1  7412  pitonn  7996  frecuzrdgtcl  10594  frecuzrdgfunlem  10601  zfz1iso  11023  shftfn  11250  exmidunben  12912  prdsex  13216  imasex  13252  imasaddfnlemg  13261  lssex  14231  tgcl  14651  epttop  14677  neissex  14752  uptx  14861  dvfgg  15275  2spim  15902  decidr  15932  bj-om  16072  bj-nnord  16093  bj-inf2vn  16109  bj-inf2vn2  16110  bj-findis  16114  exmidsbthrlem  16163  sbthom  16167