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

Theorem 2eximi 1537
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 1536 . 2 (∃𝑦𝜑 → ∃𝑦𝜓)
32eximi 1536 1 (∃𝑥𝑦𝜑 → ∃𝑥𝑦𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wex 1426
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-ial 1472
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  excomim  1598  cgsex2g  2655  cgsex4g  2656  vtocl2  2674  vtocl3  2675  dtruarb  4026  opelopabsb  4087  mosubopt  4503  xpmlem  4852  brabvv  5695  ssoprab2i  5737  dmaddpqlem  6934  nqpi  6935  dmaddpq  6936  dmmulpq  6937  enq0sym  6989  enq0ref  6990  enq0tr  6991  nq0nn  6999  prarloc  7060  bj-inex  11753
  Copyright terms: Public domain W3C validator