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  2816  elex2  2817  spcimdv  2888  spcimedv  2890  pm13.183  2942  sbcthdv  3044  sbcimdv  3095  ssrdv  3231  ss2abdv  3298  abssdv  3299  opprc  3881  dfnfc2  3909  intss  3947  intab  3955  dfiin2g  4001  disjss1  4068  mpteq12dva  4168  el  4266  exmid1dc  4288  exmidn0m  4289  exmid0el  4292  exmidundif  4294  exmidundifim  4295  exmid1stab  4296  euotd  4345  reusv1  4553  elirr  4637  sucprcreg  4645  en2lp  4650  tfisi  4683  ssrelrel  4824  issref  5117  iotaval  5296  iota5  5306  iotabidv  5307  funmo  5339  funco  5364  funun  5368  fununfun  5370  fununi  5395  funcnvuni  5396  funimaexglem  5410  fvssunirng  5650  relfvssunirn  5651  sefvex  5656  nfunsn  5672  f1oresrab  5808  funoprabg  6115  uchoice  6295  mpofvex  6365  1stconst  6381  2ndconst  6382  disjxp1  6396  tfrexlem  6495  tfr1onlemsucfn  6501  tfr1onlemsucaccv  6502  tfr1onlembxssdm  6504  tfr1onlembfn  6505  tfr1onlemaccex  6509  tfr1onlemres  6510  tfrcllemsucfn  6514  tfrcllemsucaccv  6515  tfrcllembxssdm  6517  tfrcllembfn  6518  tfrcllemaccex  6522  tfrcllemres  6523  tfrcl  6525  rdgexggg  6538  rdgifnon  6540  rdgifnon2  6541  rdgivallem  6542  frecabcl  6560  frectfr  6561  frecrdg  6569  iserd  6723  modom  6989  exmidpw  7093  exmidpweq  7094  exmidpw2en  7097  fiintim  7116  fisseneq  7119  sbthlemi3  7149  finomni  7330  exmidomniim  7331  exmidomni  7332  exmidfodomrlemr  7403  exmidfodomrlemrALT  7404  exmidmotap  7470  cc1  7474  pitonn  8058  frecuzrdgtcl  10664  frecuzrdgfunlem  10671  zfz1iso  11095  shftfn  11375  exmidunben  13037  prdsex  13342  imasex  13378  imasaddfnlemg  13387  lssex  14358  tgcl  14778  epttop  14804  neissex  14879  uptx  14988  dvfgg  15402  2spim  16298  decidr  16328  bj-om  16468  bj-nnord  16489  bj-inf2vn  16505  bj-inf2vn2  16506  bj-findis  16510  exmidsbthrlem  16562  sbthom  16566