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

Theorem alrimiv 1751
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 1416 . 2 (φxφ)
2 alrimiv.1 . 2 (φψ)
31, 2alrimih 1355 1 (φxψ)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1240
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-5 1333  ax-gen 1335  ax-17 1416
This theorem is referenced by:  alrimivv  1752  nfdv  1754  axext4  2021  eqrdv  2035  abbi2dv  2153  abbi1dv  2154  elex22  2563  elex2  2564  spcimdv  2631  spcimedv  2633  pm13.183  2675  sbcthdv  2772  sbcimdv  2817  ssrdv  2945  ss2abdv  3007  abssdv  3008  opprc  3561  dfnfc2  3589  intss  3627  intab  3635  dfiin2g  3681  disjss1  3742  mpteq12dva  3829  el  3922  euotd  3982  reusv1  4156  elirr  4224  sucprcreg  4227  en2lp  4232  tfisi  4253  ssrelrel  4383  issref  4650  iotaval  4821  iota5  4830  iotabidv  4831  funmo  4860  funco  4883  funun  4887  fununi  4910  funcnvuni  4911  funimaexglem  4925  fvssunirng  5133  relfvssunirn  5134  sefvex  5139  nfunsn  5150  f1oresrab  5272  funoprabg  5542  mpt2fvex  5771  1stconst  5784  2ndconst  5785  tfrexlem  5889  rdgexggg  5904  rdgifnon  5906  rdgifnon2  5907  rdgivallem  5908  frectfr  5924  frecrdg  5931  iserd  6068  pitonn  6724  frecuzrdgrrn  8855  frec2uzrdg  8856  frecuzrdgrom  8857  frecuzrdgfn  8859  frecuzrdgsuc  8862  2spim  9221  bj-om  9371  bj-inf2vn  9404  bj-inf2vn2  9405  bj-findis  9409
  Copyright terms: Public domain W3C validator