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  5644  relfvssunirn  5645  sefvex  5650  nfunsn  5666  f1oresrab  5802  funoprabg  6109  uchoice  6289  mpofvex  6357  1stconst  6373  2ndconst  6374  disjxp1  6388  tfrexlem  6486  tfr1onlemsucfn  6492  tfr1onlemsucaccv  6493  tfr1onlembxssdm  6495  tfr1onlembfn  6496  tfr1onlemaccex  6500  tfr1onlemres  6501  tfrcllemsucfn  6505  tfrcllemsucaccv  6506  tfrcllembxssdm  6508  tfrcllembfn  6509  tfrcllemaccex  6513  tfrcllemres  6514  tfrcl  6516  rdgexggg  6529  rdgifnon  6531  rdgifnon2  6532  rdgivallem  6533  frecabcl  6551  frectfr  6552  frecrdg  6560  iserd  6714  exmidpw  7081  exmidpweq  7082  exmidpw2en  7085  fiintim  7104  fisseneq  7107  sbthlemi3  7137  finomni  7318  exmidomniim  7319  exmidomni  7320  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  exmidmotap  7458  cc1  7462  pitonn  8046  frecuzrdgtcl  10646  frecuzrdgfunlem  10653  zfz1iso  11076  shftfn  11351  exmidunben  13013  prdsex  13318  imasex  13354  imasaddfnlemg  13363  lssex  14334  tgcl  14754  epttop  14780  neissex  14855  uptx  14964  dvfgg  15378  2spim  16213  decidr  16243  bj-om  16383  bj-nnord  16404  bj-inf2vn  16420  bj-inf2vn2  16421  bj-findis  16425  exmidsbthrlem  16478  sbthom  16482