Theorem 2exbii 1399

Description: Inference adding 2 existential quantifiers to both sides of an equivalence.

Hypothesis

Ref	Expression
2exbii.1	|- (ph <-> ps)

Assertion

Ref	Expression
2exbii	|- (E.xE.yph <-> E.xE.yps)

Proof of Theorem 2exbii

Step	Hyp	Ref	Expression
1		2exbii.1	. . 3 |- (ph <-> ps)
2	1	exbii 1398	. 2 |- (E.yph <-> E.yps)
3	2	exbii 1398	1 |- (E.xE.yph <-> E.xE.yps)

Syntax hints:   <-> wb 163  E.wex 1326

This theorem is referenced by:  3exbii 1400  3exdistr 1693  cbvex4v 1705  ee4anv 1710  sbel2x 1736  2eu4 1856  2eu6 1858  rexcom 2243  reean 2247  reeanOLD 2248  ceqsex3v 2330  ceqsex4v 2331  ceqsex8v 2333  vtocl3 2342  copsexg 3537  opabidOLD 3558  opelopabsb 3564  opabn0 3575  uniuni 3806  elxp3 4049  elvv 4053  elvvv 4054  elcnv2 4138  cnvuni 4147  coass 4415  fununi 4481  dfoprab2 4917  dmoprab 4931  rnoprab 4933  resoprab 4938  fnoprv 4946  oprabex3 4951  oprabval3 4959  oprabval6g 4962  xpcomen 5498  xpassen 5500  zorn2lem6 5955  genpn0 6258  genpass 6264  addcompr 6275  mulcompr 6277  distrlem5pr 6283  ltresr 6410  axaddopr 6417  axmulopr 6418  replim 8011  nvvcop 9545  5oalem7 11240  bnj912 12822  bnj997 12873  bnj600 13308  bnj983 13357  bnj986 13360  bnj996 13362  bnj1008 13373  bnj1021 13380  wfrlem4 13960  heiborlem24 15978  pm11.52 16342  2exanali 16343  pm11.6 16349  pm11.7 16353

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-4 1319  ax-5o 1321

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327

Copyright terms: Public domain