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  1934  cbvalvw  1969  axext4  2216  eqrdv  2230  abbi2dv  2353  abbi1dv  2354  elex22  2829  elex2  2830  spcimdv  2901  spcimedv  2903  pm13.183  2955  sbcthdv  3057  sbcimdv  3108  ssrdv  3244  ss2abdv  3311  abssdv  3312  opprc  3904  dfnfc2  3932  intss  3970  intab  3978  dfiin2g  4024  disjss1  4091  mpteq12dva  4191  el  4291  exmid1dc  4313  exmidn0m  4314  exmid0el  4317  exmidundif  4319  exmidundifim  4320  exmid1stab  4321  euotd  4371  reusv1  4579  elirr  4663  sucprcreg  4671  en2lp  4676  tfisi  4709  ssrelrel  4850  issref  5145  iotaval  5324  iota5  5334  iotabidv  5335  funmo  5367  funco  5392  funun  5397  fununfun  5399  fununi  5424  funcnvuni  5425  funimaexglem  5439  fvssunirng  5685  relfvssunirn  5686  sefvex  5691  nfunsn  5707  f1oresrab  5842  funoprabg  6152  uchoice  6331  mpofvex  6401  1stconst  6417  2ndconst  6418  disjxp1  6432  tfrexlem  6565  tfr1onlemsucfn  6571  tfr1onlemsucaccv  6572  tfr1onlembxssdm  6574  tfr1onlembfn  6575  tfr1onlemaccex  6579  tfr1onlemres  6580  tfrcllemsucfn  6584  tfrcllemsucaccv  6585  tfrcllembxssdm  6587  tfrcllembfn  6588  tfrcllemaccex  6592  tfrcllemres  6593  tfrcl  6595  rdgexggg  6608  rdgifnon  6610  rdgifnon2  6611  rdgivallem  6612  frecabcl  6630  frectfr  6631  frecrdg  6639  iserd  6793  modom  7061  exmidpw  7168  exmidpweq  7169  exmidpw2en  7172  fiintim  7191  fisseneq  7195  sbthlemi3  7229  finomni  7431  exmidomniim  7432  exmidomni  7433  exmidfodomrlemr  7505  exmidfodomrlemrALT  7506  exmidmotap  7575  cc1  7579  pitonn  8163  frecuzrdgtcl  10774  frecuzrdgfunlem  10781  zfz1iso  11213  shftfn  11509  ballotfilem2  13142  exmidunben  13177  prdsex  13482  imasex  13518  imasaddfnlemg  13527  lssex  14502  tgcl  14929  epttop  14955  neissex  15030  uptx  15139  dvfgg  15553  upgrspanop  16278  umgrspanop  16279  usgrspanop  16280  2spim  16538  decidr  16568  bj-om  16707  bj-nnord  16728  bj-inf2vn  16744  bj-inf2vn2  16745  bj-findis  16749  exmidsbthrlem  16802  sbthom  16806