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

Theorem 2eximi 1508
Description: Inference adding 2 existential quantifiers to antecedent and consequent. (Contributed by NM, 3-Feb-2005.)
Hypothesis
Ref Expression
eximi.1 (𝜑𝜓)
Assertion
Ref Expression
2eximi (∃𝑥𝑦𝜑 → ∃𝑥𝑦𝜓)

Proof of Theorem 2eximi
StepHypRef Expression
1 eximi.1 . . 3 (𝜑𝜓)
21eximi 1507 . 2 (∃𝑦𝜑 → ∃𝑦𝜓)
32eximi 1507 1 (∃𝑥𝑦𝜑 → ∃𝑥𝑦𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wex 1397
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-ial 1443
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  excomim  1569  cgsex2g  2607  cgsex4g  2608  vtocl2  2626  vtocl3  2627  dtruarb  3970  opelopabsb  4025  mosubopt  4433  xpmlem  4772  brabvv  5579  ssoprab2i  5621  dmaddpqlem  6533  nqpi  6534  dmaddpq  6535  dmmulpq  6536  enq0sym  6588  enq0ref  6589  enq0tr  6590  nq0nn  6598  prarloc  6659  bj-inex  10414
  Copyright terms: Public domain W3C validator