Theorem 2exbii 1093

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

Syntax hints:   <-> wb 153  E.wex 1021

This theorem is referenced by:  3exbi 1094  cbvex4v 1364  ee4anv 1367  sbel2x 1387  2eu4 1495  2eu6 1497  rexcom 1822  reeanv 1825  opabid 2866  opabn0 2880  uniuni 2937  elxp3 3281  elvv 3285  elcnv2 3351  cnvuni 3358  coass 3569  fununi 3620  dfoprab2 4049  dmoprab 4060  rnoprab 4062  resoprab 4067  fnoprval 4075  oprabex3 4080  oprabval3 4088  oprabval6g 4090  1st2val 4153  2nd2val 4154  xpcomen 4502  xpassen 4504  zorn2lem6 4855  genpn0 5171  genpass 5177  addcompr 5188  mulcompr 5190  distrlem5pr 5196  ltresr 5323  axaddopr 5330  axmulopr 5331  replim 6851  nvvcop 8297  5oalem7 9688

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1004  ax-4 1014  ax-5o 1016

This theorem depends on definitions:  df-bi 154  df-an 232  df-ex 1022

Copyright terms: Public domain