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

Theorem exlimddv 1866
 Description: Existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 15-Jun-2016.)
Hypotheses
Ref Expression
exlimddv.1
exlimddv.2
Assertion
Ref Expression
exlimddv
Distinct variable groups:   ,   ,
Allowed substitution hint:   ()

Proof of Theorem exlimddv
StepHypRef Expression
1 exlimddv.1 . 2
2 exlimddv.2 . . . 4
32ex 114 . . 3
43exlimdv 1787 . 2
51, 4mpd 13 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103  wex 1469 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie2 1471  ax-17 1503 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  fvmptdv2  5522  tfrlemi14d  6242  tfrexlem  6243  tfr1onlemres  6258  tfrcllemres  6271  tfrcldm  6272  erref  6461  xpdom2  6737  dom0  6744  xpen  6751  mapdom1g  6753  phplem4dom  6768  phplem4on  6773  fidceq  6775  dif1en  6785  fin0  6791  fin0or  6792  isinfinf  6803  infm  6810  en2eqpr  6813  fiuni  6883  supelti  6906  djudom  6995  difinfsn  7002  enomnilem  7031  enmkvlem  7054  enwomnilem  7062  exmidfodomrlemim  7086  exmidaclem  7093  cc2lem  7127  cc3  7129  genpml  7378  genpmu  7379  ltexprlemm  7461  ltexprlemfl  7470  ltexprlemfu  7472  suplocsr  7670  axpre-suploc  7763  eqord1  8298  nn1suc  8792  seq3f1oleml  10336  zfz1isolem1  10644  ennnfonelemim  12009  exmidunben  12011  enctlem  12017  ctiunct  12025  unct  12027  omctfn  12028  omiunct  12029  lmff  12493  txcn  12519  suplociccreex  12846  suplociccex  12847  subctctexmid  13413  exmidsbthrlem  13436  sbthom  13440
 Copyright terms: Public domain W3C validator