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

Theorem alrimiv 1768
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 1433 . 2 (𝜑 → ∀𝑥𝜑)
2 alrimiv.1 . 2 (𝜑𝜓)
31, 2alrimih 1372 1 (𝜑 → ∀𝑥𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1255
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-5 1350  ax-gen 1352  ax-17 1433
This theorem is referenced by:  alrimivv  1769  nfdv  1771  axext4  2038  eqrdv  2052  abbi2dv  2170  abbi1dv  2171  elex22  2584  elex2  2585  spcimdv  2652  spcimedv  2654  pm13.183  2701  sbcthdv  2798  sbcimdv  2848  ssrdv  2976  ss2abdv  3038  abssdv  3039  opprc  3595  dfnfc2  3623  intss  3661  intab  3669  dfiin2g  3715  disjss1  3776  mpteq12dva  3863  el  3956  euotd  4016  reusv1  4215  elirr  4291  sucprcreg  4298  en2lp  4303  tfisi  4335  ssrelrel  4465  issref  4732  iotaval  4903  iota5  4912  iotabidv  4913  funmo  4942  funco  4965  funun  4969  fununi  4992  funcnvuni  4993  funimaexglem  5007  fvssunirng  5215  relfvssunirn  5216  sefvex  5221  nfunsn  5232  f1oresrab  5354  funoprabg  5625  mpt2fvex  5854  1stconst  5867  2ndconst  5868  tfrexlem  5976  rdgexggg  5992  rdgifnon  5994  rdgifnon2  5995  rdgivallem  5996  frectfr  6013  frecrdg  6020  iserd  6160  pitonn  6952  frecuzrdgrrn  9323  frec2uzrdg  9324  frecuzrdgrom  9325  frecuzrdgfn  9327  frecuzrdgsuc  9330  shftfn  9617  2spim  10236  bj-om  10391  bj-nnord  10413  bj-inf2vn  10429  bj-inf2vn2  10430  bj-findis  10434
  Copyright terms: Public domain W3C validator