Theorem alrimiv 1885

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

Syntax hints:   → wi 4  ∀wal 1362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1458  ax-gen 1460  ax-17 1537

This theorem is referenced by:  alrimivv  1886  nfdv  1888  sbbidv  1896  cbvalvw  1931  axext4  2177  eqrdv  2191  abbi2dv  2312  abbi1dv  2313  elex22  2775  elex2  2776  spcimdv  2844  spcimedv  2846  pm13.183  2898  sbcthdv  3000  sbcimdv  3051  ssrdv  3185  ss2abdv  3252  abssdv  3253  opprc  3825  dfnfc2  3853  intss  3891  intab  3899  dfiin2g  3945  disjss1  4012  mpteq12dva  4110  el  4207  exmid1dc  4229  exmidn0m  4230  exmid0el  4233  exmidundif  4235  exmidundifim  4236  exmid1stab  4237  euotd  4283  reusv1  4489  elirr  4573  sucprcreg  4581  en2lp  4586  tfisi  4619  ssrelrel  4759  issref  5048  iotaval  5226  iota5  5236  iotabidv  5237  funmo  5269  funco  5294  funun  5298  fununi  5322  funcnvuni  5323  funimaexglem  5337  fvssunirng  5569  relfvssunirn  5570  sefvex  5575  nfunsn  5589  f1oresrab  5723  funoprabg  6017  uchoice  6190  mpofvex  6256  1stconst  6274  2ndconst  6275  disjxp1  6289  tfrexlem  6387  tfr1onlemsucfn  6393  tfr1onlemsucaccv  6394  tfr1onlembxssdm  6396  tfr1onlembfn  6397  tfr1onlemaccex  6401  tfr1onlemres  6402  tfrcllemsucfn  6406  tfrcllemsucaccv  6407  tfrcllembxssdm  6409  tfrcllembfn  6410  tfrcllemaccex  6414  tfrcllemres  6415  tfrcl  6417  rdgexggg  6430  rdgifnon  6432  rdgifnon2  6433  rdgivallem  6434  frecabcl  6452  frectfr  6453  frecrdg  6461  iserd  6613  exmidpw  6964  exmidpweq  6965  exmidpw2en  6968  fiintim  6985  fisseneq  6988  sbthlemi3  7018  finomni  7199  exmidomniim  7200  exmidomni  7201  exmidfodomrlemr  7262  exmidfodomrlemrALT  7263  exmidmotap  7321  cc1  7325  pitonn  7908  frecuzrdgtcl  10483  frecuzrdgfunlem  10490  zfz1iso  10912  shftfn  10968  exmidunben  12583  prdsex  12880  imasex  12888  imasaddfnlemg  12897  lssex  13850  tgcl  14232  epttop  14258  neissex  14333  uptx  14442  dvfgg  14842  2spim  15258  decidr  15288  bj-om  15429  bj-nnord  15450  bj-inf2vn  15466  bj-inf2vn2  15467  bj-findis  15471  exmidsbthrlem  15512  sbthom  15516