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

Theorem alrimiv 1736
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 (φxψ)
Distinct variable group:   φ,x
Allowed substitution hint:   ψ(x)

Proof of Theorem alrimiv
StepHypRef Expression
1 ax-17 1400 . 2 (φxφ)
2 alrimiv.1 . 2 (φψ)
31, 2alrimih 1338 1 (φxψ)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1226
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-5 1316  ax-gen 1318  ax-17 1400
This theorem is referenced by:  alrimivv  1737  nfdv  1739  axext4  2006  eqrdv  2020  abbi2dv  2138  abbi1dv  2139  elex22  2546  elex2  2547  spcimdv  2614  spcimedv  2616  pm13.183  2658  sbcthdv  2755  sbcimdv  2800  ssrdv  2928  ss2abdv  2990  abssdv  2991  opprc  3544  dfnfc2  3572  intss  3610  intab  3618  dfiin2g  3664  disjss1  3725  mpteq12dva  3812  el  3905  euotd  3965  reusv1  4140  elirr  4208  sucprcreg  4211  en2lp  4216  tfisi  4237  ssrelrel  4367  issref  4634  iotaval  4805  iota5  4814  iotabidv  4815  funmo  4843  funco  4866  funun  4870  fununi  4893  funcnvuni  4894  funimaexglem  4908  fvssunirng  5115  relfvssunirn  5116  sefvex  5121  nfunsn  5132  f1oresrab  5254  funoprabg  5523  mpt2fvex  5752  1stconst  5765  2ndconst  5766  tfrexlem  5870  rdgexggg  5884  rdgi0g  5886  rdgifnon  5887  rdgivallem  5888  frectfr  5900  iserd  6043  2spim  7013  bj-om  7159  bj-inf2vn  7192  bj-inf2vn2  7193  bj-findis  7197
  Copyright terms: Public domain W3C validator