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

Theorem rexlimddv 2431
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 2428 . 2 (φ → (x A ψχ))
41, 3mpd 13 1 (φχ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   wcel 1390  wrex 2301
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 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-17 1416  ax-ial 1424  ax-i5r 1425
This theorem depends on definitions:  df-bi 110  df-nf 1347  df-ral 2305  df-rex 2306
This theorem is referenced by:  grprinvlem  5637  grpridd  5639  tfrlemisucaccv  5880  tfrexlem  5889  prarloclemarch2  6402  addlocpr  6518  nqprl  6532  appdiv0nq  6544  prmuloc  6546  mullocpr  6551  ltprordil  6564  ltaddpr  6570  ltexprlemopl  6574  ltexprlemopu  6576  ltexprlemloc  6580  ltexprlemrl  6583  ltexprlemru  6585  addcanprleml  6587  addcanprlemu  6588  ltaprlem  6590  ltaprg  6591  recexprlemloc  6602  recexprlem1ssl  6604  recexprlem1ssu  6605  aptiprleml  6610  aptiprlemu  6611  ltmprr  6613  archpr  6614  cauappcvgprlemopl  6617  cauappcvgprlemopu  6619  cauappcvgprlemloc  6623  cauappcvgprlem1  6630  cauappcvgprlem2  6631  axarch  6753  readdcan  6930  cnegex  6966  addcan  6968  addcan2  6969  negeu  6979  ltadd2  7192  recexre  7342  rimul  7349  ltmul1  7356  mulap0  7397  mulcanapd  7404
  Copyright terms: Public domain W3C validator