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 ⊢ (𝜑 → ∀𝑥𝜓)

Syntax hints:   → wi 4  ∀wal 1400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1500  ax-gen 1502  ax-17 1579

This theorem is referenced 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  3920  dfnfc2  3948  intss  3986  intab  3994  dfiin2g  4040  disjss1  4107  mpteq12dva  4207  el  4310  exmid1dc  4332  exmidn0m  4333  exmid0el  4336  exmidundif  4338  exmidundifim  4339  exmid1stab  4340  euotd  4390  reusv1  4599  elirr  4683  sucprcreg  4691  en2lp  4696  tfisi  4729  ssrelrel  4870  issref  5165  iotaval  5344  iota5  5354  iotabidv  5355  funmo  5387  funco  5412  funun  5417  fununfun  5419  fununi  5444  funcnvuni  5445  funimaexglem  5459  fvssunirng  5705  relfvssunirn  5706  sefvex  5711  nfunsn  5727  f1oresrab  5864  funoprabg  6177  uchoice  6361  mpofvex  6431  1stconst  6447  2ndconst  6448  disjxp1  6462  tfrexlem  6595  tfr1onlemsucfn  6601  tfr1onlemsucaccv  6602  tfr1onlembxssdm  6604  tfr1onlembfn  6605  tfr1onlemaccex  6609  tfr1onlemres  6610  tfrcllemsucfn  6614  tfrcllemsucaccv  6615  tfrcllembxssdm  6617  tfrcllembfn  6618  tfrcllemaccex  6622  tfrcllemres  6623  tfrcl  6625  rdgexggg  6638  rdgifnon  6640  rdgifnon2  6641  rdgivallem  6642  frecabcl  6660  frectfr  6661  frecrdg  6669  iserd  6823  fsetdmprc0  6940  modom  7098  exmidpw  7205  exmidpweq  7206  exmidpw2en  7209  fiintim  7228  fisseneq  7232  sbthlemi3  7266  finomni  7470  exmidomniim  7471  exmidomni  7472  exmidfodomrlemr  7544  exmidfodomrlemrALT  7545  exmidmotap  7617  cc1  7621  pitonn  8205  frecuzrdgtcl  10827  frecuzrdgfunlem  10834  zfz1iso  11271  shftfn  11567  ballotfilem2  13206  exmidunben  13295  imasex  13603  imasaddfnlemg  13612  prdsex  14149  lssex  14663  tgcl  15088  epttop  15114  neissex  15189  uptx  15298  dvfgg  15712  upgrspanop  16438  umgrspanop  16439  usgrspanop  16440  2spim  16708  decidr  16738  bj-om  16877  bj-nnord  16898  bj-inf2vn  16914  bj-inf2vn2  16915  bj-findis  16919  exmidsbthrlem  16972  sbthom  16976