Theorem alrimiv 1922

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

Syntax hints:   → wi 4  ∀wal 1395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1495  ax-gen 1497  ax-17 1574

This theorem is referenced by:  alrimivv  1923  nfdv  1925  sbbidv  1933  cbvalvw  1968  axext4  2215  eqrdv  2229  abbi2dv  2350  abbi1dv  2351  elex22  2818  elex2  2819  spcimdv  2890  spcimedv  2892  pm13.183  2944  sbcthdv  3046  sbcimdv  3097  ssrdv  3233  ss2abdv  3300  abssdv  3301  opprc  3883  dfnfc2  3911  intss  3949  intab  3957  dfiin2g  4003  disjss1  4070  mpteq12dva  4170  el  4268  exmid1dc  4290  exmidn0m  4291  exmid0el  4294  exmidundif  4296  exmidundifim  4297  exmid1stab  4298  euotd  4347  reusv1  4555  elirr  4639  sucprcreg  4647  en2lp  4652  tfisi  4685  ssrelrel  4826  issref  5119  iotaval  5298  iota5  5308  iotabidv  5309  funmo  5341  funco  5366  funun  5371  fununfun  5373  fununi  5398  funcnvuni  5399  funimaexglem  5413  fvssunirng  5654  relfvssunirn  5655  sefvex  5660  nfunsn  5676  f1oresrab  5812  funoprabg  6120  uchoice  6300  mpofvex  6370  1stconst  6386  2ndconst  6387  disjxp1  6401  tfrexlem  6500  tfr1onlemsucfn  6506  tfr1onlemsucaccv  6507  tfr1onlembxssdm  6509  tfr1onlembfn  6510  tfr1onlemaccex  6514  tfr1onlemres  6515  tfrcllemsucfn  6519  tfrcllemsucaccv  6520  tfrcllembxssdm  6522  tfrcllembfn  6523  tfrcllemaccex  6527  tfrcllemres  6528  tfrcl  6530  rdgexggg  6543  rdgifnon  6545  rdgifnon2  6546  rdgivallem  6547  frecabcl  6565  frectfr  6566  frecrdg  6574  iserd  6728  modom  6994  exmidpw  7100  exmidpweq  7101  exmidpw2en  7104  fiintim  7123  fisseneq  7127  sbthlemi3  7158  finomni  7339  exmidomniim  7340  exmidomni  7341  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  exmidmotap  7480  cc1  7484  pitonn  8068  frecuzrdgtcl  10675  frecuzrdgfunlem  10682  zfz1iso  11106  shftfn  11402  exmidunben  13065  prdsex  13370  imasex  13406  imasaddfnlemg  13415  lssex  14387  tgcl  14807  epttop  14833  neissex  14908  uptx  15017  dvfgg  15431  upgrspanop  16153  umgrspanop  16154  usgrspanop  16155  2spim  16413  decidr  16443  bj-om  16583  bj-nnord  16604  bj-inf2vn  16620  bj-inf2vn2  16621  bj-findis  16625  exmidsbthrlem  16677  sbthom  16681