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

Theorem alrimiv 1846
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 1506 . 2 (𝜑 → ∀𝑥𝜑)
2 alrimiv.1 . 2 (𝜑𝜓)
31, 2alrimih 1445 1 (𝜑 → ∀𝑥𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1329
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1423  ax-gen 1425  ax-17 1506
This theorem is referenced by:  alrimivv  1847  nfdv  1849  axext4  2123  eqrdv  2137  abbi2dv  2258  abbi1dv  2259  elex22  2701  elex2  2702  spcimdv  2770  spcimedv  2772  pm13.183  2822  sbcthdv  2923  sbcimdv  2974  ssrdv  3103  ss2abdv  3170  abssdv  3171  opprc  3726  dfnfc2  3754  intss  3792  intab  3800  dfiin2g  3846  disjss1  3912  mpteq12dva  4009  el  4102  exmid1dc  4123  exmidn0m  4124  exmid0el  4127  exmidundif  4129  exmidundifim  4130  euotd  4176  reusv1  4379  elirr  4456  sucprcreg  4464  en2lp  4469  tfisi  4501  ssrelrel  4639  issref  4921  iotaval  5099  iota5  5108  iotabidv  5109  funmo  5138  funco  5163  funun  5167  fununi  5191  funcnvuni  5192  funimaexglem  5206  fvssunirng  5436  relfvssunirn  5437  sefvex  5442  nfunsn  5455  f1oresrab  5585  funoprabg  5870  mpofvex  6101  1stconst  6118  2ndconst  6119  disjxp1  6133  tfrexlem  6231  tfr1onlemsucfn  6237  tfr1onlemsucaccv  6238  tfr1onlembxssdm  6240  tfr1onlembfn  6241  tfr1onlemaccex  6245  tfr1onlemres  6246  tfrcllemsucfn  6250  tfrcllemsucaccv  6251  tfrcllembxssdm  6253  tfrcllembfn  6254  tfrcllemaccex  6258  tfrcllemres  6259  tfrcl  6261  rdgexggg  6274  rdgifnon  6276  rdgifnon2  6277  rdgivallem  6278  frecabcl  6296  frectfr  6297  frecrdg  6305  iserd  6455  exmidpw  6802  fiintim  6817  fisseneq  6820  sbthlemi3  6847  finomni  7012  exmidomniim  7013  exmidomni  7014  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  cc1  7080  pitonn  7663  frecuzrdgtcl  10192  frecuzrdgfunlem  10199  zfz1iso  10591  shftfn  10603  exmidunben  11945  tgcl  12242  epttop  12268  neissex  12343  uptx  12452  dvfgg  12835  2spim  13026  decidr  13056  bj-om  13188  bj-nnord  13209  bj-inf2vn  13225  bj-inf2vn2  13226  bj-findis  13230  exmid1stab  13248  exmidsbthrlem  13270  sbthom  13274
  Copyright terms: Public domain W3C validator