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  2845  spcimedv  2847  pm13.183  2899  sbcthdv  3001  sbcimdv  3052  ssrdv  3186  ss2abdv  3253  abssdv  3254  opprc  3826  dfnfc2  3854  intss  3892  intab  3900  dfiin2g  3946  disjss1  4013  mpteq12dva  4111  el  4208  exmid1dc  4230  exmidn0m  4231  exmid0el  4234  exmidundif  4236  exmidundifim  4237  exmid1stab  4238  euotd  4284  reusv1  4490  elirr  4574  sucprcreg  4582  en2lp  4587  tfisi  4620  ssrelrel  4760  issref  5049  iotaval  5227  iota5  5237  iotabidv  5238  funmo  5270  funco  5295  funun  5299  fununi  5323  funcnvuni  5324  funimaexglem  5338  fvssunirng  5570  relfvssunirn  5571  sefvex  5576  nfunsn  5590  f1oresrab  5724  funoprabg  6018  uchoice  6192  mpofvex  6260  1stconst  6276  2ndconst  6277  disjxp1  6291  tfrexlem  6389  tfr1onlemsucfn  6395  tfr1onlemsucaccv  6396  tfr1onlembxssdm  6398  tfr1onlembfn  6399  tfr1onlemaccex  6403  tfr1onlemres  6404  tfrcllemsucfn  6408  tfrcllemsucaccv  6409  tfrcllembxssdm  6411  tfrcllembfn  6412  tfrcllemaccex  6416  tfrcllemres  6417  tfrcl  6419  rdgexggg  6432  rdgifnon  6434  rdgifnon2  6435  rdgivallem  6436  frecabcl  6454  frectfr  6455  frecrdg  6463  iserd  6615  exmidpw  6966  exmidpweq  6967  exmidpw2en  6970  fiintim  6987  fisseneq  6990  sbthlemi3  7020  finomni  7201  exmidomniim  7202  exmidomni  7203  exmidfodomrlemr  7264  exmidfodomrlemrALT  7265  exmidmotap  7323  cc1  7327  pitonn  7910  frecuzrdgtcl  10486  frecuzrdgfunlem  10493  zfz1iso  10915  shftfn  10971  exmidunben  12586  prdsex  12883  imasex  12891  imasaddfnlemg  12900  lssex  13853  tgcl  14243  epttop  14269  neissex  14344  uptx  14453  dvfgg  14867  2spim  15328  decidr  15358  bj-om  15499  bj-nnord  15520  bj-inf2vn  15536  bj-inf2vn2  15537  bj-findis  15541  exmidsbthrlem  15582  sbthom  15586