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

Theorem alrimiv 1799
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 1462 . 2 (𝜑 → ∀𝑥𝜑)
2 alrimiv.1 . 2 (𝜑𝜓)
31, 2alrimih 1401 1 (𝜑 → ∀𝑥𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1285
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-5 1379  ax-gen 1381  ax-17 1462
This theorem is referenced by:  alrimivv  1800  nfdv  1802  axext4  2069  eqrdv  2083  abbi2dv  2203  abbi1dv  2204  elex22  2628  elex2  2629  spcimdv  2696  spcimedv  2698  pm13.183  2745  sbcthdv  2843  sbcimdv  2893  ssrdv  3020  ss2abdv  3083  abssdv  3084  opprc  3625  dfnfc2  3653  intss  3691  intab  3699  dfiin2g  3745  disjss1  3806  mpteq12dva  3893  el  3986  exmid0el  4005  exmidundif  4007  euotd  4053  reusv1  4252  elirr  4328  sucprcreg  4336  en2lp  4341  tfisi  4373  ssrelrel  4504  issref  4777  iotaval  4953  iota5  4962  iotabidv  4963  funmo  4992  funco  5015  funun  5019  fununi  5043  funcnvuni  5044  funimaexglem  5058  fvssunirng  5276  relfvssunirn  5277  sefvex  5282  nfunsn  5294  f1oresrab  5419  funoprabg  5694  mpt2fvex  5923  1stconst  5936  2ndconst  5937  tfrexlem  6046  tfr1onlemsucfn  6052  tfr1onlemsucaccv  6053  tfr1onlembxssdm  6055  tfr1onlembfn  6056  tfr1onlemaccex  6060  tfr1onlemres  6061  tfrcllemsucfn  6065  tfrcllemsucaccv  6066  tfrcllembxssdm  6068  tfrcllembfn  6069  tfrcllemaccex  6073  tfrcllemres  6074  tfrcl  6076  rdgexggg  6089  rdgifnon  6091  rdgifnon2  6092  rdgivallem  6093  frecabcl  6111  frectfr  6112  frecrdg  6120  iserd  6263  exmidpw  6569  fisseneq  6585  sbthlemi3  6604  finomni  6732  exmidomniim  6733  exmidomni  6734  exmidfodomrlemr  6764  exmidfodomrlemrALT  6765  pitonn  7321  frecuzrdgtcl  9739  frecuzrdgfunlem  9746  zfz1iso  10134  shftfn  10146  2spim  11096  decidr  11125  bj-om  11261  bj-nnord  11282  bj-inf2vn  11298  bj-inf2vn2  11299  bj-findis  11303  exmidsbthrlem  11341
  Copyright terms: Public domain W3C validator