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

Theorem alrimiv 1830
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 1491 . 2 (𝜑 → ∀𝑥𝜑)
2 alrimiv.1 . 2 (𝜑𝜓)
31, 2alrimih 1430 1 (𝜑 → ∀𝑥𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1314
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1408  ax-gen 1410  ax-17 1491
This theorem is referenced by:  alrimivv  1831  nfdv  1833  axext4  2101  eqrdv  2115  abbi2dv  2236  abbi1dv  2237  elex22  2675  elex2  2676  spcimdv  2744  spcimedv  2746  pm13.183  2796  sbcthdv  2896  sbcimdv  2946  ssrdv  3073  ss2abdv  3140  abssdv  3141  opprc  3696  dfnfc2  3724  intss  3762  intab  3770  dfiin2g  3816  disjss1  3882  mpteq12dva  3979  el  4072  exmid1dc  4093  exmidn0m  4094  exmid0el  4097  exmidundif  4099  exmidundifim  4100  euotd  4146  reusv1  4349  elirr  4426  sucprcreg  4434  en2lp  4439  tfisi  4471  ssrelrel  4609  issref  4891  iotaval  5069  iota5  5078  iotabidv  5079  funmo  5108  funco  5133  funun  5137  fununi  5161  funcnvuni  5162  funimaexglem  5176  fvssunirng  5404  relfvssunirn  5405  sefvex  5410  nfunsn  5423  f1oresrab  5553  funoprabg  5838  mpofvex  6069  1stconst  6086  2ndconst  6087  disjxp1  6101  tfrexlem  6199  tfr1onlemsucfn  6205  tfr1onlemsucaccv  6206  tfr1onlembxssdm  6208  tfr1onlembfn  6209  tfr1onlemaccex  6213  tfr1onlemres  6214  tfrcllemsucfn  6218  tfrcllemsucaccv  6219  tfrcllembxssdm  6221  tfrcllembfn  6222  tfrcllemaccex  6226  tfrcllemres  6227  tfrcl  6229  rdgexggg  6242  rdgifnon  6244  rdgifnon2  6245  rdgivallem  6246  frecabcl  6264  frectfr  6265  frecrdg  6273  iserd  6423  exmidpw  6770  fiintim  6785  fisseneq  6788  sbthlemi3  6815  finomni  6980  exmidomniim  6981  exmidomni  6982  exmidfodomrlemr  7026  exmidfodomrlemrALT  7027  pitonn  7624  frecuzrdgtcl  10153  frecuzrdgfunlem  10160  zfz1iso  10552  shftfn  10564  exmidunben  11866  tgcl  12160  epttop  12186  neissex  12261  uptx  12370  dvfgg  12753  2spim  12900  decidr  12930  bj-om  13062  bj-nnord  13083  bj-inf2vn  13099  bj-inf2vn2  13100  bj-findis  13104  exmid1stab  13122  exmidsbthrlem  13144  sbthom  13148
  Copyright terms: Public domain W3C validator