Theorem biexd 783

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

Hypotheses

Ref	Expression
biexd.1	|- (ph -> A.xph)
biexd.2	|- (ph -> (ps <-> ch))

Assertion

Ref	Expression
biexd	|- (ph -> (E.xps <-> E.xch))

Proof of Theorem biexd

Step	Hyp	Ref	Expression
1		biexd.1	. . 3 |- (ph -> A.xph)
2		biexd.2	. . 3 |- (ph -> (ps <-> ch))
3	1, 2	19.21ai 740	. 2 |- (ph -> A.x(ps <-> ch))
4		19.18 732	. 2 |- (A.x(ps <-> ch) -> (E.xps <-> E.xch))
5	3, 4	syl 12	1 |- (ph -> (E.xps <-> E.xch))

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

This theorem is referenced by:  biexdv 936  bimod 1030  birexda 1214  rexeqf 1322  zfrepclf 1477  biopabd 2101  bioprabd 3025  axrepndlem1 3738  axrepndlem2 3739  axrepnd 3740  axunndlem1 3741  axpowndlem2 3744  axpowndlem3 3745  axpowndlem4 3746  axregnd 3750  axinfndlem1 3751  axinfnd 3752  axacndlem4 3756  axacndlem5 3757  axacnd 3758

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