Theorem alrimiv 1920

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

Syntax hints:   → wi 4  ∀wal 1393

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1493  ax-gen 1495  ax-17 1572

This theorem is referenced by:  alrimivv  1921  nfdv  1923  sbbidv  1931  cbvalvw  1966  axext4  2213  eqrdv  2227  abbi2dv  2348  abbi1dv  2349  elex22  2815  elex2  2816  spcimdv  2887  spcimedv  2889  pm13.183  2941  sbcthdv  3043  sbcimdv  3094  ssrdv  3230  ss2abdv  3297  abssdv  3298  opprc  3878  dfnfc2  3906  intss  3944  intab  3952  dfiin2g  3998  disjss1  4065  mpteq12dva  4165  el  4262  exmid1dc  4284  exmidn0m  4285  exmid0el  4288  exmidundif  4290  exmidundifim  4291  exmid1stab  4292  euotd  4341  reusv1  4549  elirr  4633  sucprcreg  4641  en2lp  4646  tfisi  4679  ssrelrel  4819  issref  5111  iotaval  5290  iota5  5300  iotabidv  5301  funmo  5333  funco  5358  funun  5362  fununfun  5364  fununi  5389  funcnvuni  5390  funimaexglem  5404  fvssunirng  5642  relfvssunirn  5643  sefvex  5648  nfunsn  5664  f1oresrab  5800  funoprabg  6103  uchoice  6283  mpofvex  6351  1stconst  6367  2ndconst  6368  disjxp1  6382  tfrexlem  6480  tfr1onlemsucfn  6486  tfr1onlemsucaccv  6487  tfr1onlembxssdm  6489  tfr1onlembfn  6490  tfr1onlemaccex  6494  tfr1onlemres  6495  tfrcllemsucfn  6499  tfrcllemsucaccv  6500  tfrcllembxssdm  6502  tfrcllembfn  6503  tfrcllemaccex  6507  tfrcllemres  6508  tfrcl  6510  rdgexggg  6523  rdgifnon  6525  rdgifnon2  6526  rdgivallem  6527  frecabcl  6545  frectfr  6546  frecrdg  6554  iserd  6706  exmidpw  7070  exmidpweq  7071  exmidpw2en  7074  fiintim  7093  fisseneq  7096  sbthlemi3  7126  finomni  7307  exmidomniim  7308  exmidomni  7309  exmidfodomrlemr  7380  exmidfodomrlemrALT  7381  exmidmotap  7447  cc1  7451  pitonn  8035  frecuzrdgtcl  10634  frecuzrdgfunlem  10641  zfz1iso  11063  shftfn  11335  exmidunben  12997  prdsex  13302  imasex  13338  imasaddfnlemg  13347  lssex  14318  tgcl  14738  epttop  14764  neissex  14839  uptx  14948  dvfgg  15362  2spim  16130  decidr  16160  bj-om  16300  bj-nnord  16321  bj-inf2vn  16337  bj-inf2vn2  16338  bj-findis  16342  exmidsbthrlem  16390  sbthom  16394