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

Theorem 2exbii 1494
 Description: Inference adding 2 existential quantifiers to both sides of an equivalence. (Contributed by NM, 16-Mar-1995.)
Hypothesis
Ref Expression
exbii.1 (φψ)
Assertion
Ref Expression
2exbii (xyφxyψ)

Proof of Theorem 2exbii
StepHypRef Expression
1 exbii.1 . . 3 (φψ)
21exbii 1493 . 2 (yφyψ)
32exbii 1493 1 (xyφxyψ)
 Colors of variables: wff set class Syntax hints:   ↔ wb 98  ∃wex 1378 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-ial 1424 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  3exbii  1495  19.42vvvv  1787  3exdistr  1789  cbvex4v  1802  ee4anv  1806  ee8anv  1807  sbel2x  1871  2eu4  1990  rexcomf  2466  reean  2472  ceqsex3v  2590  ceqsex4v  2591  ceqsex8v  2593  copsexg  3972  opelopabsbALT  3987  opabm  4008  uniuni  4149  rabxp  4323  elxp3  4337  elvv  4345  elvvv  4346  rexiunxp  4421  elcnv2  4456  cnvuni  4464  coass  4782  fununi  4910  dfmpt3  4964  dfoprab2  5494  dmoprab  5527  rnoprab  5529  mpt2mptx  5537  resoprab  5539  ovi3  5579  ov6g  5580  oprabex3  5698  xpassen  6240  enq0enq  6414  enq0sym  6415  enq0tr  6417  ltresr  6736
 Copyright terms: Public domain W3C validator