Theorem alrimiv 1847

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

Syntax hints:   → wi 4  ∀wal 1330

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1424  ax-gen 1426  ax-17 1507

This theorem is referenced by:  alrimivv  1848  nfdv  1850  axext4  2124  eqrdv  2138  abbi2dv  2259  abbi1dv  2260  elex22  2704  elex2  2705  spcimdv  2773  spcimedv  2775  pm13.183  2826  sbcthdv  2927  sbcimdv  2978  ssrdv  3108  ss2abdv  3175  abssdv  3176  opprc  3734  dfnfc2  3762  intss  3800  intab  3808  dfiin2g  3854  disjss1  3920  mpteq12dva  4017  el  4110  exmid1dc  4131  exmidn0m  4132  exmid0el  4135  exmidundif  4137  exmidundifim  4138  euotd  4184  reusv1  4387  elirr  4464  sucprcreg  4472  en2lp  4477  tfisi  4509  ssrelrel  4647  issref  4929  iotaval  5107  iota5  5116  iotabidv  5117  funmo  5146  funco  5171  funun  5175  fununi  5199  funcnvuni  5200  funimaexglem  5214  fvssunirng  5444  relfvssunirn  5445  sefvex  5450  nfunsn  5463  f1oresrab  5593  funoprabg  5878  mpofvex  6109  1stconst  6126  2ndconst  6127  disjxp1  6141  tfrexlem  6239  tfr1onlemsucfn  6245  tfr1onlemsucaccv  6246  tfr1onlembxssdm  6248  tfr1onlembfn  6249  tfr1onlemaccex  6253  tfr1onlemres  6254  tfrcllemsucfn  6258  tfrcllemsucaccv  6259  tfrcllembxssdm  6261  tfrcllembfn  6262  tfrcllemaccex  6266  tfrcllemres  6267  tfrcl  6269  rdgexggg  6282  rdgifnon  6284  rdgifnon2  6285  rdgivallem  6286  frecabcl  6304  frectfr  6305  frecrdg  6313  iserd  6463  exmidpw  6810  fiintim  6825  fisseneq  6828  sbthlemi3  6855  finomni  7020  exmidomniim  7021  exmidomni  7022  exmidfodomrlemr  7075  exmidfodomrlemrALT  7076  cc1  7097  pitonn  7680  frecuzrdgtcl  10216  frecuzrdgfunlem  10223  zfz1iso  10616  shftfn  10628  exmidunben  11975  tgcl  12272  epttop  12298  neissex  12373  uptx  12482  dvfgg  12865  2spim  13144  decidr  13174  bj-om  13306  bj-nnord  13327  bj-inf2vn  13343  bj-inf2vn2  13344  bj-findis  13348  exmid1stab  13368  exmidsbthrlem  13392  sbthom  13396