Theorem bi2ex 734

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

Hypothesis

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

Assertion

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

Proof of Theorem bi2ex

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

Syntax hints:   <-> wb 127  E.wex 678

This theorem is referenced by:  bi3ex 735  cbvex4v 979  ee4anv 982  sbel2x 995  2eu4 1070  rexcom 1313  reeanv 1316  opabid 2099  elxp3 2460  elvv 2464  cbvop 2473  elcnv2 2515  cnvuni 2521  coass 2667  fununi 2705  dfoprab2 3021  dmoprab 3031  rnoprab 3033  fnoprval 3042  oprabex3 3046  oprabval3 3052  1st2val 3097  xpcomen 3343  xpassen 3344  zornlem6 3608  genpn0 3900  genpass 3906  addcompr 3917  mulcompr 3919  distrlem5pr 3925  ltresr 4052  replimt 4798  5oalem7 5550

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679

metamath.org