Theorem exbid 1822

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 1810	. 2 |- ( ph -> A. x ph )
3		exbid.2	. 2 |- ( ph -> ( ps <-> ch ) )
4	2, 3	exbidh 1644	1 |- ( ph -> ( E. x ps <-> E. x ch ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-12 1794

This theorem depends on definitions:  df-bi 185  df-ex 1588  df-nf 1591

This theorem is referenced by:  mobid  2282  rexbida  2844  rexeqf  3012  opabbid  4454  zfrepclf  4509  dfid3  4737  oprabbid  6240  axrepndlem1  8859  axrepndlem2  8860  axrepnd  8861  axpowndlem2  8865  axpowndlem2OLD  8866  axpowndlem3  8867  axpowndlem3OLD  8868  axpowndlem4  8869  axregnd  8873  axregndOLD  8874  axinfndlem1  8875  axinfnd  8876  axacndlem4  8880  axacndlem5  8881  axacnd  8882  opabdm  26079  opabrn  26080  fpwrelmapffslem  26168  pm14.122b  29817  pm14.123b  29820