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

Theorem 2eximi 1565
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 1564 . 2 (∃𝑦𝜑 → ∃𝑦𝜓)
32eximi 1564 1 (∃𝑥𝑦𝜑 → ∃𝑥𝑦𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wex 1453
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-4 1472  ax-ial 1499
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  excomim  1626  cgsex2g  2696  cgsex4g  2697  vtocl2  2715  vtocl3  2716  dtruarb  4085  opelopabsb  4152  mosubopt  4574  xpmlem  4929  brabvv  5785  ssoprab2i  5828  dmaddpqlem  7153  nqpi  7154  dmaddpq  7155  dmmulpq  7156  enq0sym  7208  enq0ref  7209  enq0tr  7210  nq0nn  7218  prarloc  7279  bj-inex  13032
  Copyright terms: Public domain W3C validator