Theorem alrimiv 1927

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1500  ax-gen 1502  ax-17 1579

This theorem is used by:  alrimivv  1928  nfdv  1930  sbbidv  1939  cbvalvw  1975  axext4  2222  eqrdv  2236  abbi2dv  2359  abbi1dv  2360  elex22  2837  elex2  2838  spcimdv  2909  spcimedv  2911  pm13.183  2964  sbcthdv  3066  sbcimdv  3117  ssrdv  3254  ss2abdv  3321  abssdv  3322  opprc  3925  dfnfc2  3953  intss  3991  intab  3999  dfiin2g  4045  disjss1  4112  mpteq12dva  4212  el  4315  exmid1dc  4337  exmidn0m  4338  exmid0el  4341  exmidundif  4343  exmidundifim  4344  exmid1stab  4345  euotd  4395  reusv1  4604  elirr  4688  sucprcreg  4696  en2lp  4701  tfisi  4734  ssrelrel  4875  issref  5170  iotaval  5349  iota5  5359  iotabidv  5360  funmo  5392  funco  5417  funun  5422  fununfun  5424  fununi  5449  funcnvuni  5450  funimaexglem  5464  fvssunirng  5710  relfvssunirn  5711  sefvex  5716  nfunsn  5733  f1oresrab  5873  funoprabg  6187  uchoice  6371  mpofvex  6441  1stconst  6457  2ndconst  6458  disjxp1  6472  tfrexlem  6605  tfr1onlemsucfn  6611  tfr1onlemsucaccv  6612  tfr1onlembxssdm  6614  tfr1onlembfn  6615  tfr1onlemaccex  6619  tfr1onlemres  6620  tfrcllemsucfn  6624  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllembfn  6628  tfrcllemaccex  6632  tfrcllemres  6633  tfrcl  6635  rdgexggg  6648  rdgifnon  6650  rdgifnon2  6651  rdgivallem  6652  frecabcl  6670  frectfr  6671  frecrdg  6679  iserd  6833  fsetdmprc0  6950  modom  7108  exmidpw  7215  exmidpweq  7216  exmidpw2en  7219  fiintim  7238  fisseneq  7242  sbthlemi3  7276  finomni  7480  exmidomniim  7481  exmidomni  7482  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  exmidmotap  7627  cc1  7631  pitonn  8215  frecuzrdgtcl  10849  frecuzrdgfunlem  10856  zfz1iso  11293  shftfn  11589  ballotfilem2  13228  exmidunben  13317  imasex  13626  imasaddfnlemg  13635  prdsex  14172  lssex  14691  tgcl  15165  epttop  15191  neissex  15266  uptx  15375  dvfgg  15789  upgrspanop  16524  umgrspanop  16525  usgrspanop  16526  2spim  16794  decidr  16824  bj-om  16963  bj-nnord  16984  bj-inf2vn  17000  bj-inf2vn2  17001  bj-findis  17005  exmidsbthrlem  17067  sbthom  17071