Theorem exbid 1829

Description: Formula-building rule for existential quantifier (deduction rule). (Contributed by Mario Carneiro, 24-Sep-2016.)

Hypotheses

Ref	Expression
exbid.1	|- F/ x ph
exbid.2	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
exbid	|- ( ph -> ( E. x ps <-> E. x ch ) )

Proof of Theorem exbid

Step	Hyp	Ref	Expression
1		exbid.1	. . 3 |- F/ x ph
2	1	nfri 1817	. 2 |- ( ph -> A. x ph )
3		exbid.2	. 2 |- ( ph -> ( ps <-> ch ) )
4	2, 3	exbidh 1648	1 |- ( ph -> ( E. x ps <-> E. x ch ) )

Syntax hints:   -> wi 4   <-> wb 184   E.wex 1591   F/wnf 1594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-12 1798

This theorem depends on definitions:  df-bi 185  df-ex 1592  df-nf 1595

This theorem is referenced by:  mobid  2292  rexbida  2963  rexeqf  3050  opabbid  4504  zfrepclf  4559  dfid3  4791  oprabbid  6327  axrepndlem1  8958  axrepndlem2  8959  axrepnd  8960  axpowndlem2  8964  axpowndlem2OLD  8965  axpowndlem3  8966  axpowndlem3OLD  8967  axpowndlem4  8968  axregnd  8972  axregndOLD  8973  axinfndlem1  8974  axinfnd  8975  axacndlem4  8979  axacndlem5  8980  axacnd  8981  opabdm  27125  opabrn  27126  fpwrelmapffslem  27215  pm14.122b  30865  pm14.123b  30868