Theorem alrimiv 1809

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

Syntax hints:   → wi 4  ∀wal 1294

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-5 1388  ax-gen 1390  ax-17 1471

This theorem is referenced by:  alrimivv  1810  nfdv  1812  axext4  2079  eqrdv  2093  abbi2dv  2213  abbi1dv  2214  elex22  2648  elex2  2649  spcimdv  2717  spcimedv  2719  pm13.183  2768  sbcthdv  2868  sbcimdv  2918  ssrdv  3045  ss2abdv  3109  abssdv  3110  opprc  3665  dfnfc2  3693  intss  3731  intab  3739  dfiin2g  3785  disjss1  3850  mpteq12dva  3941  el  4034  exmidn0m  4054  exmid0el  4056  exmidundif  4058  exmidundifim  4059  euotd  4105  reusv1  4308  elirr  4385  sucprcreg  4393  en2lp  4398  tfisi  4430  ssrelrel  4567  issref  4847  iotaval  5025  iota5  5034  iotabidv  5035  funmo  5064  funco  5088  funun  5092  fununi  5116  funcnvuni  5117  funimaexglem  5131  fvssunirng  5355  relfvssunirn  5356  sefvex  5361  nfunsn  5373  f1oresrab  5502  funoprabg  5782  mpt2fvex  6011  1stconst  6024  2ndconst  6025  disjxp1  6039  tfrexlem  6137  tfr1onlemsucfn  6143  tfr1onlemsucaccv  6144  tfr1onlembxssdm  6146  tfr1onlembfn  6147  tfr1onlemaccex  6151  tfr1onlemres  6152  tfrcllemsucfn  6156  tfrcllemsucaccv  6157  tfrcllembxssdm  6159  tfrcllembfn  6160  tfrcllemaccex  6164  tfrcllemres  6165  tfrcl  6167  rdgexggg  6180  rdgifnon  6182  rdgifnon2  6183  rdgivallem  6184  frecabcl  6202  frectfr  6203  frecrdg  6211  iserd  6358  exmidpw  6704  fiintim  6719  fisseneq  6722  sbthlemi3  6748  finomni  6883  exmidomniim  6884  exmidomni  6885  exmidfodomrlemr  6925  exmidfodomrlemrALT  6926  pitonn  7482  frecuzrdgtcl  9968  frecuzrdgfunlem  9975  zfz1iso  10361  shftfn  10373  tgcl  11916  epttop  11942  neissex  12017  2spim  12375  decidr  12404  bj-om  12540  bj-nnord  12561  bj-inf2vn  12577  bj-inf2vn2  12578  bj-findis  12582  exmidsbthrlem  12617