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

Theorem rexlimddv 2411
Description: Restricted existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 15-Jun-2016.)
Hypotheses
Ref Expression
rexlimddv.1 (φx A ψ)
rexlimddv.2 ((φ (x A ψ)) → χ)
Assertion
Ref Expression
rexlimddv (φχ)
Distinct variable groups:   φ,x   χ,x
Allowed substitution hints:   ψ(x)   A(x)

Proof of Theorem rexlimddv
StepHypRef Expression
1 rexlimddv.1 . 2 (φx A ψ)
2 rexlimddv.2 . . 3 ((φ (x A ψ)) → χ)
32rexlimdvaa 2408 . 2 (φ → (x A ψχ))
41, 3mpd 13 1 (φχ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   wcel 1370  wrex 2281
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1312  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-4 1377  ax-17 1396  ax-ial 1405  ax-i5r 1406
This theorem depends on definitions:  df-bi 110  df-nf 1326  df-ral 2285  df-rex 2286
This theorem is referenced by:  grprinvlem  5614  grpridd  5616  tfrlemisucaccv  5856  tfrexlem  5866  prarloclemarch2  6270  addlocpr  6385  appdiv0nq  6402  prmuloc  6404  mullocpr  6409  ltprordil  6422  ltaddpr  6428  ltexprlemopl  6432  ltexprlemopu  6434  ltexprlemloc  6438  ltexprlemrl  6441  ltexprlemru  6443  addcanprleml  6445  addcanprlemu  6446  ltaprlem  6448  ltaprg  6449  recexprlemloc  6459  recexprlem1ssl  6461  recexprlem1ssu  6462  readdcan  6740  cnegex  6776  addcan  6778  addcan2  6779  negeu  6789  ltadd2  7002
  Copyright terms: Public domain W3C validator