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

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

Proof of Theorem rexlimddv
StepHypRef Expression
1 rexlimddv.1 . 2
2 rexlimddv.2 . . 3
32rexlimdvaa 2428 . 2
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  6519  nqprl  6533  appdiv0nq  6545  prmuloc  6547  mullocpr  6552  ltprordil  6565  ltaddpr  6571  ltexprlemopl  6575  ltexprlemopu  6577  ltexprlemloc  6581  ltexprlemrl  6584  ltexprlemru  6586  addcanprleml  6588  addcanprlemu  6589  ltaprlem  6591  ltaprg  6592  recexprlemloc  6603  recexprlem1ssl  6605  recexprlem1ssu  6606  aptiprleml  6611  aptiprlemu  6612  ltmprr  6614  archpr  6615  cauappcvgprlemopl  6618  cauappcvgprlemopu  6620  cauappcvgprlemloc  6624  cauappcvgprlem1  6631  cauappcvgprlem2  6632  caucvgprlemopl  6640  caucvgprlemopu  6642  caucvgprlemloc  6646  caucvgprlem2  6651  axarch  6773  readdcan  6950  cnegex  6986  addcan  6988  addcan2  6989  negeu  6999  ltadd2  7212  recexre  7362  rimul  7369  ltmul1  7376  mulap0  7417  mulcanapd  7424
  Copyright terms: Public domain W3C validator