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  2173  eqrdv  2187  abbi2dv  2308  abbi1dv  2309  elex22  2767  elex2  2768  spcimdv  2836  spcimedv  2838  pm13.183  2890  sbcthdv  2992  sbcimdv  3043  ssrdv  3176  ss2abdv  3243  abssdv  3244  opprc  3814  dfnfc2  3842  intss  3880  intab  3888  dfiin2g  3934  disjss1  4001  mpteq12dva  4099  el  4193  exmid1dc  4215  exmidn0m  4216  exmid0el  4219  exmidundif  4221  exmidundifim  4222  exmid1stab  4223  euotd  4269  reusv1  4473  elirr  4555  sucprcreg  4563  en2lp  4568  tfisi  4601  ssrelrel  4741  issref  5026  iotaval  5204  iota5  5213  iotabidv  5214  funmo  5246  funco  5271  funun  5275  fununi  5299  funcnvuni  5300  funimaexglem  5314  fvssunirng  5545  relfvssunirn  5546  sefvex  5551  nfunsn  5564  f1oresrab  5697  funoprabg  5990  mpofvex  6222  1stconst  6240  2ndconst  6241  disjxp1  6255  tfrexlem  6353  tfr1onlemsucfn  6359  tfr1onlemsucaccv  6360  tfr1onlembxssdm  6362  tfr1onlembfn  6363  tfr1onlemaccex  6367  tfr1onlemres  6368  tfrcllemsucfn  6372  tfrcllemsucaccv  6373  tfrcllembxssdm  6375  tfrcllembfn  6376  tfrcllemaccex  6380  tfrcllemres  6381  tfrcl  6383  rdgexggg  6396  rdgifnon  6398  rdgifnon2  6399  rdgivallem  6400  frecabcl  6418  frectfr  6419  frecrdg  6427  iserd  6579  exmidpw  6926  exmidpweq  6927  fiintim  6946  fisseneq  6949  sbthlemi3  6976  finomni  7156  exmidomniim  7157  exmidomni  7158  exmidfodomrlemr  7219  exmidfodomrlemrALT  7220  exmidmotap  7278  cc1  7282  pitonn  7865  frecuzrdgtcl  10430  frecuzrdgfunlem  10437  zfz1iso  10839  shftfn  10851  exmidunben  12445  prdsex  12740  imasex  12748  imasaddfnlemg  12757  lssex  13631  tgcl  13961  epttop  13987  neissex  14062  uptx  14171  dvfgg  14554  2spim  14915  decidr  14945  bj-om  15086  bj-nnord  15107  bj-inf2vn  15123  bj-inf2vn2  15124  bj-findis  15128  exmidsbthrlem  15168  sbthom  15172