Theorem 2exbidv 1281

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

Hypothesis

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

Assertion

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

Distinct variable groups:   ph,x   ph,y

Proof of Theorem 2exbidv

Step	Hyp	Ref	Expression
1		2albidv.1	. . 3 |- (ph -> (ps <-> ch))
2	1	exbidv 1279	. 2 |- (ph -> (E.yps <-> E.ych))
3	2	exbidv 1279	1 |- (ph -> (E.xE.yps <-> E.xE.ych))

Syntax hints:   -> wi 3   <-> wb 146  E.wex 980

This theorem is referenced by:  3exbidv 1282  4exbidv 1283  cbvex4v 1322  copsexg 2792  elopab 2811  relop 3275  cbvoprab3v 4000  oprabval6g 4032  th3qlem1 4314  genpv 5102  genpelv 5103  genpprecl 5104  genpnnp 5108  genpass 5112  distrlem1pr 5127  distrlem5pr 5131  ltresr 5258  bsi 10495

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975

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

Copyright terms: Public domain