Theorem alrimiv 1923

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

Syntax hints:   → wi 4  ∀wal 1396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1496  ax-gen 1498  ax-17 1575

This theorem is referenced by:  alrimivv  1924  nfdv  1926  sbbidv  1935  cbvalvw  1971  axext4  2218  eqrdv  2232  abbi2dv  2355  abbi1dv  2356  elex22  2831  elex2  2832  spcimdv  2903  spcimedv  2905  pm13.183  2958  sbcthdv  3060  sbcimdv  3111  ssrdv  3248  ss2abdv  3315  abssdv  3316  opprc  3910  dfnfc2  3938  intss  3976  intab  3984  dfiin2g  4030  disjss1  4097  mpteq12dva  4197  el  4297  exmid1dc  4319  exmidn0m  4320  exmid0el  4323  exmidundif  4325  exmidundifim  4326  exmid1stab  4327  euotd  4377  reusv1  4585  elirr  4669  sucprcreg  4677  en2lp  4682  tfisi  4715  ssrelrel  4856  issref  5151  iotaval  5330  iota5  5340  iotabidv  5341  funmo  5373  funco  5398  funun  5403  fununfun  5405  fununi  5430  funcnvuni  5431  funimaexglem  5445  fvssunirng  5691  relfvssunirn  5692  sefvex  5697  nfunsn  5713  f1oresrab  5848  funoprabg  6161  uchoice  6345  mpofvex  6415  1stconst  6431  2ndconst  6432  disjxp1  6446  tfrexlem  6579  tfr1onlemsucfn  6585  tfr1onlemsucaccv  6586  tfr1onlembxssdm  6588  tfr1onlembfn  6589  tfr1onlemaccex  6593  tfr1onlemres  6594  tfrcllemsucfn  6598  tfrcllemsucaccv  6599  tfrcllembxssdm  6601  tfrcllembfn  6602  tfrcllemaccex  6606  tfrcllemres  6607  tfrcl  6609  rdgexggg  6622  rdgifnon  6624  rdgifnon2  6625  rdgivallem  6626  frecabcl  6644  frectfr  6645  frecrdg  6653  iserd  6807  modom  7075  exmidpw  7182  exmidpweq  7183  exmidpw2en  7186  fiintim  7205  fisseneq  7209  sbthlemi3  7243  finomni  7445  exmidomniim  7446  exmidomni  7447  exmidfodomrlemr  7519  exmidfodomrlemrALT  7520  exmidmotap  7592  cc1  7596  pitonn  8180  frecuzrdgtcl  10802  frecuzrdgfunlem  10809  zfz1iso  11242  shftfn  11538  ballotfilem2  13177  exmidunben  13266  imasex  13574  imasaddfnlemg  13583  prdsex  14119  lssex  14633  tgcl  15060  epttop  15086  neissex  15161  uptx  15270  dvfgg  15684  upgrspanop  16409  umgrspanop  16410  usgrspanop  16411  2spim  16679  decidr  16709  bj-om  16848  bj-nnord  16869  bj-inf2vn  16885  bj-inf2vn2  16886  bj-findis  16890  exmidsbthrlem  16943  sbthom  16947