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

Theorem 2eximi 1611
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 1610 . 2 (∃𝑦𝜑 → ∃𝑦𝜓)
32eximi 1610 1 (∃𝑥𝑦𝜑 → ∃𝑥𝑦𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wex 1502
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1457  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-4 1520  ax-ial 1544
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  excomim  1673  cgsex2g  2785  cgsex4g  2786  vtocl2  2804  vtocl3  2805  dtruarb  4203  opelopabsb  4272  mosubopt  4703  xpmlem  5061  brabvv  5934  ssoprab2i  5977  dmaddpqlem  7390  nqpi  7391  dmaddpq  7392  dmmulpq  7393  enq0sym  7445  enq0ref  7446  enq0tr  7447  nq0nn  7455  prarloc  7516  bj-inex  14955
  Copyright terms: Public domain W3C validator