Theorem bi2exdv 938

Description: Formula-building rule for 2 existential quantifiers (deduction rule).

Hypothesis

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

Assertion

Ref	Expression
bi2exdv	|- (ph -> (E.xE.yps <-> E.xE.ych))

Distinct variable group(s):   ph,x   ph,y

Proof of Theorem bi2exdv

Step	Hyp	Ref	Expression
1		bi2aldv.1	. . 3 |- (ph -> (ps <-> ch))
2	1	biexdv 936	. 2 |- (ph -> (E.yps <-> E.ych))
3	2	biexdv 936	1 |- (ph -> (E.xE.yps <-> E.xE.ych))

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

This theorem is referenced by:  bi3exdv 939  bi4exdv 940  cbvex4v 979  copsexg 1902  elopab 2110  cbvoprab3v 3030  th3qlem1 3250  genpv 3896  genpelv 3897  genpprecl 3898  genpnnp 3902  genpass 3906  distrlem1pr 3921  distrlem5pr 3925  ltresr 4052

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  ax-17 925

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

metamath.org