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

Theorem alrimiv 1796
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 1460 . 2 (𝜑 → ∀𝑥𝜑)
2 alrimiv.1 . 2 (𝜑𝜓)
31, 2alrimih 1399 1 (𝜑 → ∀𝑥𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1283
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-5 1377  ax-gen 1379  ax-17 1460
This theorem is referenced by:  alrimivv  1797  nfdv  1799  axext4  2066  eqrdv  2080  abbi2dv  2198  abbi1dv  2199  elex22  2615  elex2  2616  spcimdv  2683  spcimedv  2685  pm13.183  2733  sbcthdv  2830  sbcimdv  2880  ssrdv  3006  ss2abdv  3068  abssdv  3069  opprc  3599  dfnfc2  3627  intss  3665  intab  3673  dfiin2g  3719  disjss1  3780  mpteq12dva  3867  el  3960  euotd  4017  reusv1  4216  elirr  4292  sucprcreg  4300  en2lp  4305  tfisi  4336  ssrelrel  4466  issref  4737  iotaval  4908  iota5  4917  iotabidv  4918  funmo  4947  funco  4970  funun  4974  fununi  4998  funcnvuni  4999  funimaexglem  5013  fvssunirng  5221  relfvssunirn  5222  sefvex  5227  nfunsn  5239  f1oresrab  5361  funoprabg  5631  mpt2fvex  5860  1stconst  5873  2ndconst  5874  tfrexlem  5983  tfr1onlemsucfn  5989  tfr1onlemsucaccv  5990  tfr1onlembxssdm  5992  tfr1onlembfn  5993  tfr1onlemaccex  5997  tfr1onlemres  5998  tfrcllemsucfn  6002  tfrcllemsucaccv  6003  tfrcllembxssdm  6005  tfrcllembfn  6006  tfrcllemaccex  6010  tfrcllemres  6011  tfrcl  6013  rdgexggg  6026  rdgifnon  6028  rdgifnon2  6029  rdgivallem  6030  frecabcl  6048  frectfr  6049  frecrdg  6057  iserd  6198  pitonn  7078  frecuzrdgtcl  9494  frecuzrdgfunlem  9501  shftfn  9850  2spim  10728  decidr  10757  bj-om  10890  bj-nnord  10911  bj-inf2vn  10927  bj-inf2vn2  10928  bj-findis  10932
  Copyright terms: Public domain W3C validator