ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  alrimiv GIF version

Theorem alrimiv 1861
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
StepHypRef Expression
1 ax-17 1513 . 2 (𝜑 → ∀𝑥𝜑)
2 alrimiv.1 . 2 (𝜑𝜓)
31, 2alrimih 1456 1 (𝜑 → ∀𝑥𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1340
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1434  ax-gen 1436  ax-17 1513
This theorem is referenced by:  alrimivv  1862  nfdv  1864  cbvalvw  1906  axext4  2148  eqrdv  2162  abbi2dv  2283  abbi1dv  2284  elex22  2737  elex2  2738  spcimdv  2806  spcimedv  2808  pm13.183  2860  sbcthdv  2961  sbcimdv  3012  ssrdv  3144  ss2abdv  3211  abssdv  3212  opprc  3774  dfnfc2  3802  intss  3840  intab  3848  dfiin2g  3894  disjss1  3960  mpteq12dva  4058  el  4152  exmid1dc  4174  exmidn0m  4175  exmid0el  4178  exmidundif  4180  exmidundifim  4181  euotd  4227  reusv1  4431  elirr  4513  sucprcreg  4521  en2lp  4526  tfisi  4559  ssrelrel  4699  issref  4981  iotaval  5159  iota5  5168  iotabidv  5169  funmo  5198  funco  5223  funun  5227  fununi  5251  funcnvuni  5252  funimaexglem  5266  fvssunirng  5496  relfvssunirn  5497  sefvex  5502  nfunsn  5515  f1oresrab  5645  funoprabg  5933  mpofvex  6164  1stconst  6181  2ndconst  6182  disjxp1  6196  tfrexlem  6294  tfr1onlemsucfn  6300  tfr1onlemsucaccv  6301  tfr1onlembxssdm  6303  tfr1onlembfn  6304  tfr1onlemaccex  6308  tfr1onlemres  6309  tfrcllemsucfn  6313  tfrcllemsucaccv  6314  tfrcllembxssdm  6316  tfrcllembfn  6317  tfrcllemaccex  6321  tfrcllemres  6322  tfrcl  6324  rdgexggg  6337  rdgifnon  6339  rdgifnon2  6340  rdgivallem  6341  frecabcl  6359  frectfr  6360  frecrdg  6368  iserd  6519  exmidpw  6866  exmidpweq  6867  fiintim  6886  fisseneq  6889  sbthlemi3  6916  finomni  7096  exmidomniim  7097  exmidomni  7098  exmidfodomrlemr  7150  exmidfodomrlemrALT  7151  cc1  7198  pitonn  7781  frecuzrdgtcl  10338  frecuzrdgfunlem  10345  zfz1iso  10744  shftfn  10756  exmidunben  12322  tgcl  12631  epttop  12657  neissex  12732  uptx  12841  dvfgg  13224  2spim  13509  decidr  13539  bj-om  13681  bj-nnord  13702  bj-inf2vn  13718  bj-inf2vn2  13719  bj-findis  13723  exmid1stab  13742  exmidsbthrlem  13763  sbthom  13767
  Copyright terms: Public domain W3C validator