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

Theorem 2eximi 1563
 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 1562 . 2 (∃𝑦𝜑 → ∃𝑦𝜓)
32eximi 1562 1 (∃𝑥𝑦𝜑 → ∃𝑥𝑦𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4  ∃wex 1451 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-ial 1497 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  excomim  1624  cgsex2g  2693  cgsex4g  2694  vtocl2  2712  vtocl3  2713  dtruarb  4075  opelopabsb  4142  mosubopt  4564  xpmlem  4917  brabvv  5771  ssoprab2i  5814  dmaddpqlem  7133  nqpi  7134  dmaddpq  7135  dmmulpq  7136  enq0sym  7188  enq0ref  7189  enq0tr  7190  nq0nn  7198  prarloc  7259  bj-inex  12797
 Copyright terms: Public domain W3C validator