Theorem 2exbii 1048

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 1047	. 2 |- (E.yph <-> E.yps)
3	2	exbii 1047	1 |- (E.xE.yph <-> E.xE.yps)

Syntax hints:   <-> wb 146  E.wex 977

This theorem is referenced by:  3exbi 1049  cbvex4v 1317  ee4anv 1320  sbel2x 1340  2eu4 1445  2eu6 1447  rexcom 1767  reeanv 1770  opabid 2799  opabn0 2813  uniuni 2870  elxp3 3214  elvv 3218  elcnv2 3283  cnvuni 3290  coass 3498  fununi 3549  dfoprab2 3976  dmoprab 3987  rnoprab 3989  resoprab 3994  fnoprval 4002  oprabex3 4007  oprabval3 4015  oprabval6g 4017  1st2val 4079  2nd2val 4080  xpcomen 4419  xpassen 4421  zorn2lem6 4765  genpn0 5078  genpass 5084  addcompr 5095  mulcompr 5097  distrlem5pr 5103  ltresr 5230  axaddopr 5237  axmulopr 5238  replimt 6692  nvvcop 8151  5oalem7 9522

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-4 970  ax-5o 972

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978

Copyright terms: Public domain